Re: [isabelle] Trying to fit HOL to traditional math verbiage

On Sat, Nov 5, 2011 at 5:21 PM, James Frank <james.isa at> wrote:
> I'm not used to a character that's been defined as an operator being used by
> itself to refer to a function. Even now, I know I can talk of "comp", but I
> don't know if I can talk of "o" without using it with f and g. In Haskell I
> can refer to + by putting it in (+). All this would feel second nature if I
> had been doing much coding and using functions like sum(a,b) instead of
> "a+b".
> That's all notation, it's six of one, or a half dozen of the other.

You're right, it's just syntax. You can talk about o on its own by
putting it in brackets (o), just like + in Haskell. (o) is the same
thing as comp.

> _Q1_: Have you seen it [composition] being defined as a function before? If
> so, what was
> its domain and range?
> It's always defined as a function, where a function is a set of ordered
> pairs. If g:A-->B and f:B-->C, then the domain and range are determined for
> (f o g). We have to have (f o g):A-->C, where A, B, and C can be any sets.

No. I was asking whether you'd seen composition itself, just the (o),
defined as a function before. You're saying that the result of
composition, f o g, is always a function. That's right. But I guess
usually you would think of the "o" there as an operator that can never
appear on its own without two arguments around it. From the
higher-order perspective, as you've noticed, all of these are
functions: "_ o _", "f o _", "_ o g", and "f o g". The first one takes
two functions and returns a function. The second two take one function
and return a function. The last one takes something (maybe not a
function, depends on g) and returns something else (again, depends on

> _Q2_:(I also want to ask: how would you usually think of an ordinary
> function that takes two arguments? This line would continue into a
> discussion about currying, but I'll leave it out for now.)
> As a two variable function f(x,y).
> But it's not acceptable for me to think like that now. When I was studying
> functional programming for practical reasons, it was acceptable to think of
> "f: 'a =>  'b =>  'c" as a two variable function f(a,b), but once you make
> it part of a math definition, I'm only allowed to to think of it as what it
> is.

There are at least three ways to think about functions of multiple arguments.

1) Have a new variation on the theme of "function" for every number of
arguments it might take, so a function of two arguments is a different
although similar kind of entity as a function of one argument. It
might be a set of triples as opposed to a set of pairs, for example.

2) (Curried functions) Every function takes exactly one argument. To
get the effect of taking more arguments, return a function to consume
the remaining arguments. For example, suppose we have f(x,y) = x + y.
As a curried function, f would have type num => num => num, or, for
clarity, num => (num => num). When you apply it to one argument, it
returns a function of type num => num. Thus f 3 :: num => num. Now if
you apply that resulting function to one argument, it returns a
number. (f 3) 4 :: num (and (f 3) 4 = 7). We would usually write f 3 4
for (f 3) 4, by making function application associate to the left.

3) Every function takes exactly one argument. To get the effect of
taking more arguments, take all your required arguments at once in a
tuple. The function f as above would in this case have type num * num
=> num. You apply it to a pair of numbers (3,4), and get back a number
f (3,4) = 7.

Representations 2 and 3 are closely related. Indeed, you can write a
(higher-order) function to transform a curried function into an
uncurried function (and vice versa).

Are any of these close to how you usually think of functions of
multiple arguments?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.