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



Again, I didn't hit the right reply button on a previous reply, so I put this back public. In my reply to Piotr, I said complementary things about both Mizar and Isabelle. Personally, I'd like to learn all the proof assistants, just for the fun of it.

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

Thanks for your reply. I will post your text to the Mizar forum (I hope I do not need your permission to do this).

Recently, there are initiatives within Mizar to add something like Sledgehammer and initial experiments are quite encouraging, at least for me. Have a look at http://pxtp2011.loria.fr/ for a paper by Josef Urban and me.

I have been in Mizar since its conception and the stress has been on developing the language and the library. The efforts towards automation of proofs and searches have been neglected for far too long.

Cheers, PR

On 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>





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