*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*: Tue, 8 Nov 2011 08:12:00 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4EB81E84.8090606@gmx.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> <4EB81E84.8090606@gmx.com>*Sender*: ramana.kumar at gmail.com

On Mon, Nov 7, 2011 at 6:08 PM, James Frank <james.isa at gmx.com> wrote: > Ramana, > 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. Good. I'm glad they were both familiar already. > 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? I'm not sure what you mean. You said "or" between two things that would go together. I think the answer is "no". > 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. Functions are fundamental to HOL, so you're right if you're calling that the "compiler level". (But you don't have to go to the ML compiler level!) The function type operator (the "=>" we were using before) is primitive, that is, not created by type definition. In the usual model of HOL in set theory, it constructs function spaces.

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

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

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

- 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