Re: [isabelle] Trying to fit HOL to traditional math verbiage
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
We have the following typings
f :: 'b => 'c
g :: 'a => 'b
comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
comp f :: ('a => 'b) => 'a => 'c
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