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



Ramana,

Thanks for answering anyway, but this shows that a big part of the battle is getting the notation down. At least I was right that there are 4 functions instead of 3 (though I was actually wrong in the total number, as I discovered below).

I'm not used to a character that's been defined as an operator being used by itself to refer to a function. Even now, I know I can talk of "comp", but I don't know if I can talk of "o" without using it with f and g. In Haskell I can refer to + by putting it in (+). All this would feel second nature if I had been doing much coding and using functions like sum(a,b) instead of "a+b".

That's all notation, it's six of one, or a half dozen of the other.

However, there's "comp", "comp f", and "comp f g", and those variations are related to currying and the nifty things currying allows you to do when defining other functions with "comp", as I understand it.

First, I don't know how to use "comp f g x", where to put the parentheses, but that's trivial, and shows I haven't worked far enough into the basic tutorials.

More importantly, I'm trying to figure out what the simple analogy is between set based function composition and functional programming function composition. My short answer guess is, "There is no simple analogy to be made using the set function composition notation and the functional programming function composition notation". Yes, they accomplish the same thing, but no, they're not close enough. Their notational similarities will hurt you and make a fool out of you.

Currying allows me to specify 3 related functions, "comp", "comp f", and "comp f g". Wait. I need a fourth function which involves a variable...

But, no, it's even worse, now that I've studied your comments below more. You listed five functions:
      f :: 'b => 'c
      g :: 'a => 'b
      comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
      comp f :: ('a => 'b) => 'a => 'c
      comp f g :: 'a => 'c

But that's helpful, along with comment on following the "type path". I think it's a little clearer now that the lambda notation is just a way to specify the path that x::`a follows when used as an argument for g.

It's currying. It can't be something else. That's why you guys immediately tied my questions into currying.

But now, to answer your two questions:

_Q1_: Have you seen it [composition] being defined as a function before? If so, what was
its domain and range?

It's always defined as a function, where a function is a set of ordered pairs. If g:A-->B and f:B-->C, then the domain and range are determined for (f o g). We have to have (f o g):A-->C, where A, B, and C can be any sets.

_Q2_:(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.)

As a two variable function f(x,y).

But it's not acceptable for me to think like that now. When I was studying functional programming for practical reasons, it was acceptable to think of "f: 'a =>  'b =>  'c" as a two variable function f(a,b), but once you make it part of a math definition, I'm only allowed to to think of it as what it is.

The only option is to set up an equivalence that allows me to think the way I want to think.

Thanks for the help,
--James




On 11/4/2011 3:27 PM, Ramana Kumar wrote:
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







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