*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*: Sat, 05 Nov 2011 12:21:30 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

Ramana,

That's all notation, it's six of one, or a half dozen of the other.

f :: 'b => 'c g :: 'a => 'b comp :: ('b => 'c) => ('a => 'b) => 'a => 'c comp f :: ('a => 'b) => 'a => 'c comp f g :: 'a => 'c

But now, to answer your two questions: _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. _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. The only option is to set up an equivalence that allows me to think the way I want to think. Thanks for the help, --James On 11/4/2011 3:27 PM, Ramana Kumar wrote:

On Fri, Nov 4, 2011 at 5:46 PM, James Frank<james.isa at gmx.com> wrote:Have you seen it [composition] being defined as a function before? If so, what was its domain and range? (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.)I could restate the essence of my first email: Currying is not a problem. It not being a part of the math literature is a problem. I don't understand currying because I wasn't taught currying. My math professors didn't teach me currying because they didn't understand currying. Most likely, they were very happy knowing nothing about currying. Most likely, they will die happy knowing nothing about currying. That's not a problem unless I want them to read something that I write that involves currying, but I will, or someone like them, so it's a problem.It's not too hard. I would encourage you to answer my two questions above.For example, when I use "comp f g" in my mind rather than "f o g", it gives me better understanding.I agree. (That's why I like Lisp's syntax, or rather, lack of syntax.)I think I had figured out that the whole thing, "('b => 'c) => ('a => 'b) => 'a => 'c" is (%x. f(g x)), or "f o g", though initially I was mistaking (%x. f(g x)) for the function of type ('a => `c), since in a traditional definition if g:A-->B and f: B-->C, then (f o g):A-->C.You got it right the first time. The type of (%x. f (g x)) is 'a => 'c.But if "f" is the function of type ('b => 'c), "g" is the function of type ('a => 'b), and (%x. f(g x)) is the function of type "('b => 'c) => ('a => 'b) => 'a => 'c", then who is that function of type ('a => `c)?Since "%x. f (g x)" is the function of type 'a => 'c (and it is equal by definition to "f o g"), the question should perhaps be what is the function of type "('b => 'c) => ('a => 'b) => 'a => 'c"? And the answer, as I mentioned before, is "comp". Let's see how this works in full detail. We have the following typings f :: 'b => 'c g :: 'a => 'b comp :: ('b => 'c) => ('a => 'b) => 'a => 'c therefore comp f :: ('a => 'b) => 'a => 'c and thus comp f g :: 'a => 'c Done. For extra practice, consider the definition of "comp f g". It was given as "%x. f (g x)", and we now know that it is a function of type 'a => 'c. That means "x" has type 'a, and f (g x) has type 'c. And indeed that checks out: x :: 'a, so g x :: 'b, so f (g x) :: 'c

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

**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

- 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