*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Mon, 07 Nov 2011 12:08:04 -0600*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAMej=25frc7c9CUTVHqrQKiJ0AbHVy21spKBVkbEX46GrbCbpg@mail.gmail.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com> <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@mail.gmail.com> <4EB5709A.3090203@gmx.com> <CAMej=25frc7c9CUTVHqrQKiJ0AbHVy21spKBVkbEX46GrbCbpg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

Ramana,

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?

**Follow-Ups**:**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Previous by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list