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



Ramana,

Thanks again for the help. I'll answer your last question first, and then go long-winded on you.

_Q_: 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?

Yes, #3 pretty much represents multi-variable calculus. It's all about having a function f:R^n --> R^m. N-tuples. It's all about n-tuples.

As to currying, in the Haskell books, it was quickly pointed out that though curried functions were primarily being used, as you say, which they said, going back and forth between curried functions and uncurried functions is not a problem. All these details about curried functions will help me if curried functions become a part of what I'm doing.

However, the reason that we're having to talk about multi-variable functions, in relation to function composition, is not because of how function composition is implemented with sets, but how it's implemented without sets.

The definition of sets function composition doesn't make it a function which takes multiple arguments. If the domain is a collection of n-tuples, then we have a multi-variable function. If not... I always get paranoid when making technical claims, even if they're basic.

I'll stop here. All I have to do flip a mental switch. Initially, I make it my goal to prove every theorem in Rudin just like he does. If I flip a switch, then I decide it's good to implement them with proofs founded on curried functions.

But I still have questions, which you don't need to answer. Are curried functions merely part of implementation, or can they be abstracted out?

Where am I going to find the definition of function? I see that function is already being used in Fun.thy. I see that Groups.thy is two levels up from HOL.thy, and functions are used in groups. My guess is that I'm going to find function at the compiler level.

Thanks,
James




On 11/6/2011 6:22 AM, Ramana Kumar wrote:
On Sat, Nov 5, 2011 at 5:21 PM, James Frank<james.isa at gmx.com>  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
f).

_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.