*To*: James Frank <james.isa at gmx.com>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Fri, 4 Nov 2011 01:19:40 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4EB2E13B.507@gmx.com>*References*: <4EB2E13B.507@gmx.com>*Sender*: ramana.kumar at gmail.com

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 gmx.com> 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").

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

- Previous by Date: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: [isabelle] Four job opportunities in York
- Previous by Thread: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list