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

There are many ways to go about answering your question, and I'm sure
other people on the list will make better attempts than me. But I hope
multiple answers will help you, at least for different perspectives.
The main thing I want to say is that I think the situation is
salvageable: functional programming, (simple) type theory, and lambda
calculus are not so far removed from traditional mathematics.
You may be interested also in looking at Higher Order Set Theory. But
for now let's stick with HOL.
I'll make a few specific comments below, under the relevant bits of
your message.

On Thu, Nov 3, 2011 at 6:45 PM, James Frank <james.isa at> wrote:
> My question, stated very general, is this: "Can I take a file such as
> ~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard
> math definitions and theorems, with a few changes to accommodate types, and
> have these standard definitions/theorems be describing the same objects as
> the Isabelle definitions and lemma?" I'm not talking about starting with a
> different logical framework or set of axioms, and ending up at the same
> place.

I think yes.

> Functions have domains and ranges. You won't be surprised here, but never
> once have I seen "function composition" be defined with the domain being a
> set of functions, and the range being a set of functions whose elements are
> functions, which take functions, and return functions.

Have you seen it 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.)

> Here's what I want out of "definition comp", using more standard math
> language:
> DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o g):'a-->'b,
> where (f o g)(x) = f(g(x)).

This looks like a definition of composition as an "operator", rather
than a function. From a "first-order" perspective, since functions are
on a higher level than the values they take and receive, we need a
separate concept for things like comp that operate on functions
themselves. Notice that Definition 1.1.1 doesn't ever say that "o"
itself is taking arguments and returning a value, rather, it specifies
what the function "f o g" (which is really a function and not an
operator) does by saying what it does on arguments.

When you switch to the "higher-order" perspective, these distinctions
all disappear. Functions are values too, and operators that
take/receive functions are also just functions. So the function
composition operator is itself a function.

> Okay, what I really want is something like this:
>    (f o g) = {(a,c) in AxC | ThereExists b in B, such that (a,b) is in g and
> (b,c) is in f}.
> You can tell me different, but I assume I'm correct in saying that "comp" is
> not this set, and can't be this set, though with some work, some form of
> equivalence could be shown. Again, I guess that's right.

It could be that set in a model of HOL, but the sets in the model
wouldn't be the same as the sets encoded in Set.thy for example. To
avoid confusion, perhaps I should just say "you're right, comp is not
that set, but it is in some sense equivalent."

> POINT 1: In a standard definition of function composition, there are
> typically three functions, "f", "g", and "f o g".
> POINT2: In "comp", there are four functions, "f", "g", "(\<lambda>x. f (g
> x))", and the function of type
>    "('b => 'c)  => ('a  => 'b)  => 'a  => 'c".

The fourth function in "comp" is function composition itself (denoted by "o").

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