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

On Fri, Nov 4, 2011 at 5:46 PM, James Frank <james.isa at> 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


  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

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