Re: [isabelle] Trying to fit HOL to traditional math verbiage
Piotr Rudnicki forwarded this thread, here is my view.
I have seen the following justifications of doing formal
mathematics in simply typed HOL instead of in standard set theory:
1. Better automation of type inference
2. Better automation of (total) functions
I do not think any of them is particularly valid today. It seems
to me that they are just deeply embedded in the LCF heritage (use
of ML, etc.). Larry himself has formalized ZF quite far in Isabelle.
ad (1): Automation of type inference in existing HOL-based
systems based on Hindley-Milner is quite simple in comparison to
dependent type systems, be it done foundationally as in Coq, or
as a soft type system as in Mizar. Additional type class
systems (in Isabelle and Coq) are themselves soft type systems
grafted on top of the systems' foundational cores, already
motivated by user demand for improved (non-foundational)
ad (2): Automation of working with (not just total) functions is
again a fairly simple mechanism, implementable also in set
I think that any of the major systems (starting with Isabelle)
has today integrated much more powerful automations, based on
bridges to automated tools working in propositional and
first-order (not higher-order) logic, and its decidable
I believe that the focus on total functions as foundational
objects came from their success in programming, but it is foreign
to most of mathematics as done by mathematicians. The
set-theoretical world of HOL is different from standard set
theory. Basic set-theoretical cosnstructs like von Neuman's
ordinals do not work for HOL's standard "sets" because of the
type constraints. The universe is sparser, because its sets are
typed. When I see a set-theory-related development done
in (Isabelle/)HOL (last time this was measure theory), it leaves
me wondering about how/if various set-theoretical agendas and
their implications (e.g. the forcing methods, implications of the
axiom of choice) are answered.
To sum up: I do not think that there are good pragmatic
automation-related reasons for persuading mathematicians to work
in HOL instead of ZF. Given the very low penetration that formal
mathematics has so far among mathematicians, I think it would not
hurt the formal systems to go where the mathematicians are.
On 11/5/11, James Frank <james.isa at gmx.com> wrote:
> Thanks for answering anyway, but this shows that a big part of the
> battle is getting the notation down. At least I was right that there are
> 4 functions instead of 3 (though I was actually wrong in the total
> number, as I discovered below).
> I'm not used to a character that's been defined as an operator being
> used by itself to refer to a function. Even now, I know I can talk of
> "comp", but I don't know if I can talk of "o" without using it with f
> and g. In Haskell I can refer to + by putting it in (+). All this would
> feel second nature if I had been doing much coding and using functions
> like sum(a,b) instead of "a+b".
> That's all notation, it's six of one, or a half dozen of the other.
> However, there's "comp", "comp f", and "comp f g", and those variations
> are related to currying and the nifty things currying allows you to do
> when defining other functions with "comp", as I understand it.
> First, I don't know how to use "comp f g x", where to put the
> parentheses, but that's trivial, and shows I haven't worked far enough
> into the basic tutorials.
> More importantly, I'm trying to figure out what the simple analogy is
> between set based function composition and functional programming
> function composition. My short answer guess is, "There is no simple
> analogy to be made using the set function composition notation and the
> functional programming function composition notation". Yes, they
> accomplish the same thing, but no, they're not close enough. Their
> notational similarities will hurt you and make a fool out of you.
> Currying allows me to specify 3 related functions, "comp", "comp f", and
> "comp f g". Wait. I need a fourth function which involves a variable...
> But, no, it's even worse, now that I've studied your comments below
> more. You listed five functions:
> f :: 'b => 'c
> g :: 'a => 'b
> comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
> comp f :: ('a => 'b) => 'a => 'c
> comp f g :: 'a => 'c
> But that's helpful, along with comment on following the "type path". I
> think it's a little clearer now that the lambda notation is just a way
> to specify the path that x::`a follows when used as an argument for g.
> It's currying. It can't be something else. That's why you guys
> immediately tied my questions into currying.
> But now, to answer your two questions:
> _Q1_: Have you seen it [composition] being defined as a function before? If
> so, what was
> its domain and range?
> It's always defined as a function, where a function is a set of ordered
> pairs. If g:A-->B and f:B-->C, then the domain and range are determined for
> (f o g). We have to have (f o g):A-->C, where A, B, and C can be any sets.
> _Q2_:(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.)
> As a two variable function f(x,y).
> But it's not acceptable for me to think like that now. When I was studying
> functional programming for practical reasons, it was acceptable to think of
> "f: 'a => 'b => 'c" as a two variable function f(a,b), but once you make
> it part of a math definition, I'm only allowed to to think of it as what it
> The only option is to set up an equivalence that allows me to think the way
> I want to think.
> Thanks for the help,
> On 11/4/2011 3:27 PM, Ramana Kumar wrote:
>> On Fri, Nov 4, 2011 at 5:46 PM, James Frank<james.isa at gmx.com> wrote:
>>>> Have you seen it [composition] 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.)
>>> I could restate the essence of my first email: Currying is not a problem.
>>> not being a part of the math literature is a problem. I don't understand
>>> currying because I wasn't taught currying. My math professors didn't
>>> me currying because they didn't understand currying. Most likely, they
>>> very happy knowing nothing about currying. Most likely, they will die
>>> knowing nothing about currying. That's not a problem unless I want them
>>> read something that I write that involves currying, but I will, or
>>> like them, so it's a problem.
>> It's not too hard. I would encourage you to answer my two questions above.
>>> For example, when I use "comp f g" in my mind rather than "f o g", it
>>> me better understanding.
>> I agree. (That's why I like Lisp's syntax, or rather, lack of syntax.)
>>> I think I had figured out that the whole thing,
>>> "('b => 'c) => ('a => 'b) => 'a => 'c"
>>> is (%x. f(g x)), or "f o g", though initially I was mistaking (%x. f(g
>>> for the function of type ('a => `c), since in a traditional definition
>>> g:A-->B and f: B-->C, then (f o g):A-->C.
>> You got it right the first time. The type of (%x. f (g x)) is 'a => 'c.
>>> But if "f" is the function of type ('b => 'c), "g" is the function of
>>> ('a => 'b), and (%x. f(g x)) is the function of type "('b => 'c) =>
>>> => 'b) => 'a => 'c", then who is that function of type ('a =>
>> Since "%x. f (g x)" is the function of type 'a => 'c (and it is equal
>> by definition to "f o g"), the question should perhaps be what is the
>> function of type "('b => 'c) => ('a => 'b) => 'a => 'c"? And the
>> answer, as I mentioned before, is "comp". Let's see how this works in
>> full detail.
>> We have the following typings
>> f :: 'b => 'c
>> g :: 'a => 'b
>> comp :: ('b => 'c) => ('a => 'b) => 'a => 'c
>> comp f :: ('a => 'b) => 'a => 'c
>> and thus
>> comp f g :: 'a => 'c
>> Done. For extra practice, consider the definition of "comp f g".
>> It was given as "%x. f (g x)", and we now know that it is a function
>> of type 'a => 'c.
>> That means "x" has type 'a, and f (g x) has type 'c.
>> And indeed that checks out:
>> x :: 'a, so
>> g x :: 'b, so
>> f (g x) :: 'c
This archive was generated by a fusion of
Pipermail (Mailman edition) and