# [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.*