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

I'm not used to using "reply all", so I put this back public, along with my previous response, where I admit that it's pretty foolish to be wanting to eliminate something that's at the core. After this set, I don't want to be so guilty of cluttering up the mailing list with non-technical emails.

On 11/4/2011 6:13 PM, Lawrence Paulson wrote:
On 4 Nov 2011, at 19:31, James Frank wrote:

The problem is with this ubiquitous "'a =>  'b =>  'c" type statement. It's not a part of 98% (a little less or little more) of the math world.
I can't believe that any serious mathematician would struggle with this.

Larry Paulson

It never entered my mind that they couldn't understand it, it's my assumption that they don't even want to, especially not for me.

But that's an assumption for my purposes. You're Larry Paulson at Cambridge. You make waves. I ride waves. The only safe assumption for me is that no one is going to learn functional programming concepts for me.

We try and cater to the reader, some of us more than others. I'm trying to set myself up now to do that in the future. I see the HOL wave and the ZF wave. The HOL wave is bigger, and I want the potential support and opportunity that may come with it, so I initially pick the HOL wave.

But you make it sound simple, this transition to math heavily tied into functional programming. It's not that some of the basic concepts are rocket science, but where's the satisfaction in just having a basic, intuitive understanding of concepts? Having that attitude goes against the very core of seeking to justify everything in math.

And then there's always the person who wants to take it to the next level. It's not enough for him or her to do algebra, he or she has to go wild with categories, and make me do lots of searches to find a decent textbook on categories for self-study, when algebra is perfectly fine without another level of abstraction.

It sounds like I'm lecturing. It's not really my place to do that here, but, obviously, I'm willing to do it.


Dr. Paulson,

There is a sense in which your question is not entirely meaningful...
I can see that. It would be like me saying, "That epsilon in the definition of limit is annoying me, because it annoys my students, and they don't want to learn about epsilons. What's an easy way for me to get rid of it?"

But the realization that I was going to commit some "rigor sins" is what brought this on.

The basic idea is that I have two parallel lines of language in a document. Standard "math English", and the Isabelle code. The purpose is to help me clarify ideas, and to make the math more interesting and appealing to a typical mathematician.

There's not a problem with something like "lemma interior_ball: "x:interior S <-> (EX e>0. ball x e <= interior S)".

The problem is with this ubiquitous "'a => 'b => 'c" type statement. It's not a part of 98% (a little less or little more) of the math world.

Initially, I thought, "Okay, mask it with some other notation if you can, or talk about how, all together, the Isabelle code is equivalent to my math English".

I realized I can't do that. When I get to qed, I want to say, "Look, I've proved my math English theorem with Isabelle code." But if my math English is not a reasonable mirror of the Isabelle code, then I haven't proved anything but the Isabelle code.

It's not a real problem. I either broach a subject and give rigorous or semi-rigorous explanations, or I use certain math without explaining what I'm doing, and let the reader figure it out.

It's just that every analysis book in the world has a token introduction to set theory, functions, etc.. With math, I'm an imitator, and easily following that pattern is blown out of the water with HOL.

Anything that you can define in higher-order logic is not merely explicable in traditional mathematical terms, but it is easily so. But there are plenty of things you can write in mathematics that are impossible to formalise in higher-order logic.

The good news is that different foundations converge at a higher point where they a lot of math in common.

Again, there's no real problem. Very few people have an in-depth understanding of the foundations of math, so there's a lot of skipping that low level stuff anyway, or totally ignoring it.


On 11/4/2011 11:55 AM, Lawrence Paulson wrote:
There is a sense in which your question is not entirely meaningful, because you're asking whether rigorous but informal mathematics is adequately captured by a particular formalisation, and such issues are ultimately subjective. However, traditional mathematics is often assumed to be based on set theory, and higher-order logic has very straightforward models in set theory. In particular, if you look at the function f o g, then you get exactly the same set of ordered pairs by either route, assuming you're in the mood to interpret a function as a set of ordered pairs. The situation with higher-order logic is very different from that presented by various constructive type theories you may have seen, where you typically cannot regard a function as a set of pairs.

Some of the other points that you mention relate to basic lambda-calculus. There is no need to study the lambda calculus in its full glory, as it is quite irrelevant to higher-order logic. Lambda-notation merely expresses the notion of a function, something that is curiously lacking in standard mathematical practice. The type of the composition operator is a well-known device, known as currying, for expressing functions that take multiple arguments. Again, traditional mathematics is quite careless in such situations. You remark that functions have domains and ranges, but typically the function composition operator is not written in such terms at all, and is allowed to apply to any compatible pairs of functions whatever. In the language of set theory, it is a class function.

Anything that you can define in higher-order logic is not merely explicable in traditional mathematical terms, but it is easily so. But there are plenty of things you can write in mathematics that are impossible to formalise in higher-order logic. This is because mathematics is essentially open-ended.

Larry Paulson

On 3 Nov 2011, at 18:45, James Frank wrote:

I'll ask the easy question first. In my inbox, there's isabelle-users at and cl-isabelle-users at . 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.


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