[isabelle] Trying to fit HOL to traditional math verbiage



I'll ask the easy question first. In my inbox, there's isabelle-users at cl.cam.ac.uk and cl-isabelle-users at lists.cam.ac.uk . Does it make any difference which address I use to send in a question? If it doesn't, you don't need to answer that question.

I've tried not to ask different forms of my next question. That's because after studying enough type theory, lambda calculus, functional programming, and files from ~~/src/HOL, I'll figure out most of the answers. But that could be up to a years worth of work, and I'm trying to get a feel for where this road is going, and whether I may need to travel the road less traveled.

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.

Below I ask related questions which are probably more straight forward to answer, and, if answered, might answer the question just posed.

To get more specific, I'll ask some questions about "definition comp" in Fun.thy, which is the definition of function composition.

First, here are some related goals to set the context, for why I'm thinking about this now: 1) I want to cater to mathematicians who are doing traditional mathematics. Therefore, the language of my definitions and theorems needs to be reasonably familiar to them. I'd like to start rephrasing Isabelle defs and thms now. 2) I want to build on, and learn from, what others have done. Therefore, my first choice is HOL rather than ZF, since the library is larger, even though HOL is not as "traditional".

Here's the definition of comp from Fun.thy:

definition comp :: "('b => 'c) => ('a => 'b) => 'a => 'c" (infixl "o" 55) where
  "f o g = (\<lambda>x. f (g x))"

Studying Haskell is what led me to Isabelle, and I studied just enough functional programming to know that comp is a function that takes type "('b => 'c)" and returns type (('a => 'b) => 'a => 'c)). I guess that's right, although I ask below about (\<lambda>x. f (g x)), and about its domain and range.

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.

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)).

Notice that I tweak the definition to use types rather than sets. I was also tempted to stick "(f o g) = (%x. f(g x))" in there, not that I know much more than what it symbolizes. The details and groundwork could be worked out if it's basically the same thing as "comp".

A pertinent point here is that with a definition such as DEFINITION 1.1.1, I'm not making many demands on someone. They might be willing to go with it even with only an intuitive understanding of types and lambda calculus. However, it's important to me that something like DEFINITION 1.1.1 and "comp" be the same thing. Not be like, "think of them as the same", but "are the same".

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.

Somewhere in this question is me trying to figure out how different "comp" is from a standard definition of composition. Is "comp" close enough to a standard definition to try and phrase it using standard language, or it's "functional programming, type theory, and lambda calculus", and I should just accept it for what it is. Regardless, it is what it is, and I want to describe it as what it is, but describe it using language other than Isabelle code.

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".

What I've said above might could be summarized with this question:
What is this thing, this function "('b => 'c) => ('a => 'b) => 'a => 'c"?

If I have to incorporate that into my traditional-style definition, then it's no longer traditional-style. If I have to do that, then I'm doing something different.

If it's necessary details, and a way of specifying "g:'a-->'b, f:'b-->'c, and (f o g):'a-->'b", and I can easily formalize the connection prior to my function composition definition, then the situation is salvageable.

Anyway, feel free to comment or not.

Thanks,
James










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