*To*: Piotr Rudnicki <piotr at cs.ualberta.ca>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Sat, 05 Nov 2011 12:42:18 -0500*In-reply-to*: <CANrSq7ihHbsk8ZhbTWDzH4RD30W6ptcxVEo3q9x8jjjajnsR-g@mail.gmail.com>*References*: <4EB2E13B.507@gmx.com> <CANrSq7io9_Zdr5oAYSpZQe80NMkEXjjXo5GsXG-=uZxiymP-Jg@mail.gmail.com> <4EB42F87.1000308@gmx.com> <CANrSq7ihHbsk8ZhbTWDzH4RD30W6ptcxVEo3q9x8jjjajnsR-g@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

On 11/4/2011 3:02 PM, Piotr Rudnicki wrote:

James,Thanks for your reply. I will post your text to the Mizar forum (Ihope I do not need your permission to do this).Recently, there are initiatives within Mizar to add something likeSledgehammer and initial experiments are quite encouraging, at leastfor me. Have a look at http://pxtp2011.loria.fr/ for a paper by JosefUrban and me.I have been in Mizar since its conception and the stress has been ondeveloping the language and the library. The efforts towardsautomation of proofs and searches have been neglected for far too long.Cheers, PROn Fri, Nov 4, 2011 at 12:31 PM, James Frank <james.isa at gmx.com<mailto:james.isa at gmx.com>> wrote:Piotr, Actually, after doing a little initial research on Coq and Isabelle, I had decided to go the Mizar route for 3 main reasons: readability, it's founded on axiomatic set theory, and it has a huge library. Really, how much sweeter can it get than for a theorem prover to start with 5 axioms in the first source file, and then everything else be built on that? The point where I "closed the book" on Mizar was when I was reading a Mizar proof, while still trying to figure out if Mizar was the best way to go, and I saw that the most trivial of details had to be justified. In particular, at earlier points in the proof, something like "a = b" and "a > b" had been stated. Then there was a step where it was stated "a >= b", and that step had to be justified with some reference labels. I thought, "Do I really want to be searching for the labels for everything single thing I've stated and proved?" I had also read reviews, http://www.cs.ru.nl/~freek/comparison/index.html <http://www.cs.ru.nl/%7Efreek/comparison/index.html> (first link), about how some provers could figure out trivial details on their own. I don't particularly like "by auto" when I want proof details, but I'm glad it's there in Isabelle. Mizar is great because of all the math that's been proved with it, but some key ideas with me are "move reasonably fast" and "don't spend more of my life than necessary on data entry". I didn't choose Mizar for practical reasons, just like I choose HOL over ZF. A lot of decisions, practically speaking, are made for us. All I'm trying to do right now is annotate whatever Isabelle source code that I need to study, with standard math language. If I do that enough, and it's polished enough, it could be useful to others. You'll see that if I ask math questions, because I'll use it as part of asking questions, although I'm trying not to ask questions. It takes too much time. Other than that, I'm just operating as a student of math until I learn enough to publish something. That's where Isabelle comes in. No one will give me the time of day when it comes to checking my proofs. As consolation, I'm not the only one with that problem. -James On 11/3/2011 11:18 PM, Piotr Rudnicki wrote:Hi, Would you consider a translation from HOL to say Mizar? Mizar has been meant to mirror the everyday math vernacular. Whether the attempt has been successful or not still remains to be judged. I am interested in what you are trying to do and would like to hear what you get. Cheers, PR On Thu, Nov 3, 2011 at 12:45 PM, James Frank <james.isa at gmx.com <mailto:james.isa at gmx.com>> wrote: I'll ask the easy question first. In my inbox, there's isabelle-users at cl.cam.ac.uk <mailto:isabelle-users at cl.cam.ac.uk> and cl-isabelle-users at lists.cam.ac.uk <mailto: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--Piotr Rudnicki http://www.cs.ualberta.ca/~piotr<http://www.cs.ualberta.ca/%7Epiotr>--Piotr Rudnicki http://www.cs.ualberta.ca/~piotr<http://www.cs.ualberta.ca/%7Epiotr>

**References**:**[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: [isabelle] Four job opportunities in York
- 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