*To*: James Frank <james.isa at gmx.com>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: Josef Urban <josef.urban at gmail.com>*Date*: Sat, 5 Nov 2011 19:38:24 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Ramana Kumar <rk436 at cam.ac.uk>*In-reply-to*: <4EB5709A.3090203@gmx.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com> <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@mail.gmail.com> <4EB5709A.3090203@gmx.com>

Hi, 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) type-related automations. ad (2): Automation of working with (not just total) functions is again a fairly simple mechanism, implementable also in set theory. 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 fragments. 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. Josef On 11/5/11, James Frank <james.isa at gmx.com> wrote: > Ramana, > > 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 > is. > > The only option is to set up an equivalence that allows me to think the way > I want to think. > > Thanks for the help, > --James > > > > > 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. >>> It >>> 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 >>> teach >>> me currying because they didn't understand currying. Most likely, they >>> were >>> very happy knowing nothing about currying. Most likely, they will die >>> happy >>> knowing nothing about currying. That's not a problem unless I want them >>> to >>> read something that I write that involves currying, but I will, or >>> someone >>> 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 >>> gives >>> 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 >>> x)) >>> for the function of type ('a => `c), since in a traditional definition >>> if >>> 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 >>> type >>> ('a => 'b), and (%x. f(g x)) is the function of type "('b => 'c) => >>> ('a >>> => 'b) => 'a => 'c", then who is that function of type ('a => >>> `c)? >> 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 >> >> therefore >> >> 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 >> > > >

**Follow-Ups**:**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Jeremy Dawson

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

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

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

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Previous by Thread: Re: [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