*To*: James Frank <james.isa at gmx.com>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Fri, 4 Nov 2011 20:27:49 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4EB42510.7020408@gmx.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com>*Sender*: ramana.kumar at gmail.com

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:*James Frank

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

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: Re: [isabelle] Proof document to span multiple sessions
- 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