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

On Mon, Nov 7, 2011 at 6:08 PM, James Frank <james.isa at> 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.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.