[isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy

[Gottfried Barrow]

Hi,

I want to recover the ordered pair part of an int. I actually have a
simple solution like this:

definition myI :: "int => nat * nat" where
"myI x = (nat x, nat (-x))"

In the process of getting to the above definition, I was trying to get
the ordered pair using lower level methods. Even though I have a
solution, I ask about these other methods in case there's something
useful there for me to use.

In Int.thy, on line 20, int is defined as a quotient_type:

(020) quotient_type int = "nat * nat" / "intrel"
(021) morphisms Rep_Integ Abs_Integ

The type of Rep_Integ is (int => (nat * nat)), so I try to use it with
something like "Rep_Integ 3", but I can't ever get it to return an
ordered pair like (3,0).

QUESTION: Is there a way for me to get "Rep_Integ 3" to return (3,0)?

I try to do some lifting, like on line 208:

(208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
of_nat j"

However, on line 1661, there's this:

(1661) declare Quotient_int [quot_del]

In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
try to enable it blindly like,

setup_lifting Quotient_int,

but I get a warning, and lifting doesn't work for me.

QUESTION: Can I enable lifting for int?

Thanks,
GB

[Lawrence Paulson]

The simple answer is no. What your request is impossible. The integers are constructed as a quotient and therefore the representation of an integer is an equivalence class, in this case a set of pairs of natural numbers. The construction does not give you a map from integers to some distinguished element of this set. Of course, nothing stops you from writing your own function from integers to pairs of natural numbers.

Some time ago I wrote a paper on such matters, which you may find useful:

http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses.pdf

Larry Paulson

[Ondřej Kunčar]

On 05/21/2013 05:22 AM, Gottfried Barrow wrote:
> I try to do some lifting, like on line 208:
>
> (208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
> of_nat j"
>
> However, on line 1661, there's this:
>
> (1661) declare Quotient_int [quot_del]
>
> In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
> try to enable it blindly like,
>
> setup_lifting Quotient_int,
>
> but I get a warning, and lifting doesn't work for me.

I guess "lifting doesn't work for me" means this:

Lifting failed for the following term:
Term: λ(i∷nat, j∷nat). of_nat i - of_nat j
Type: nat × nat ⇒ ?'b∷{minus,semiring_1}

Reason: The type of the term cannot be instantiated to "nat × nat ⇒
'a∷type".

And this gives you a hint where the problem is:
you cannot instantied 'a::type for ?'b::{minus, semiring_1}.

The original definition of of_int in Int.thy is done in a context ring_1.

Try this:

lift_definition of_int :: "int => 'a::ring_1" is "%(i,j). of_nat i -
of_nat j"

> QUESTION: Can I enable lifting for int?

Yes, by the command you used:
setup_lifting Quotient_int
or even better together with the reflexivity theorem:
setup_lifting Quotient_int int_equivp[THEN equivp_reflp2]

Ondrej

[Gottfried Barrow]

Larry,

Alright, your paper will be the explanatory comments to Int.thy that
everyone forgot to put in. Your slides will also be useful:

http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses-slides.pdf
<http://www.cl.cam.ac.uk/%7Elp15/papers/Reports/equivclasses-slides.pdf>

I just need to match up a little of your notation in the paper with the
newer Isar that's in Int.thy, and a lot of the naming is the same.

It'd be interesting to know if it's common these days for other
languages to use the classic definition of the integers as equivalence
classes like you did with Int.thy:

https://en.wikipedia.org/wiki/Integer#Construction

It seems it's common for the natural numbers to be built using the
successor function, but I'm guessing it's not so common for the integers
to be equivalence classes.

I only need one representation of an integer, like (3,0) for 3, which I
can use to tie into an equivalence class of my own, if that's the way I
should do things, and it will work out.

Thanks for the help,
GB

[Johannes Hölzl]

Am Dienstag, den 21.05.2013, 22:23 -0500 schrieb Gottfried Barrow:
> It'd be interesting to know if it's common these days for other
> languages to use the classic definition of the integers as equivalence
> classes like you did with Int.thy:
>
> https://en.wikipedia.org/wiki/Integer#Construction
>
> It seems it's common for the natural numbers to be built using the
> successor function, but I'm guessing it's not so common for the integers
> to be equivalence classes.

In my experience it is quite the other way round. The first semesters
mathematics course I attended introduced the integers, the rational
numbers and the real numbers as equivalence classes. Only the natural
numbers and the complex numbers where introduced like a datatype.

- Johannes

[Lawrence Paulson]

My slides briefly hint at the reason why the integers and rationals are almost invariably defined using equivalence classes and not using particular representations such as signed natural numbers or reduced fractions. It is simply that equivalence classes make everything much easier.

Imagine defining addition on signed natural numbers. You will need at least three cases: (1) the signs agree (2) left operand is greater (3) right operand is greater. To prove the associative law, you will have four occurrences of the addition operator and therefore 81 separate cases. With equivalence classes, there is only one case and it is shown in full on one of the slides.

For fractions in reduced form, the situation is even worse, because you're constantly reasoning about greatest common divisors. With equivalent classes, there is no need for that.

Larry Paulson

[Ondřej Kunčar]

On 05/22/2013 07:13 AM, Gottfried Barrow wrote:
> Ondřej,
>
> One thing led to another, and I did a bunch of searches, and it turns
> out you would be one of the two to ask for a tutorial on lifting, but
> I'm sure you don't have time.
>
> I found this:
>
> http://www4.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf
> <http://www4.in.tum.de/%7Ekuncar/documents/huffman-kuncar-itp2012.pdf>
>
> And it turns out you have connections to Josef Urban.
>
> I got rid of my setup_lifting warning by importing Quotient_Product.thy,
> from a tip of yours here:
>
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-January/msg00127.html
>
>
> Now, I do setup_lifting, and the line of code you gave me works, so I'm
> at an error for a simple thing I want to do, which will show you that I
> have a fundamental misunderstanding of how to use lifting:
>
> setup_lifting Quotient_int
> lift_definition of_int :: "int => 'a::ring_1" is "%(i, j). of_nat i
> - of_nat j"
> by(metis int.abs_eq_iff of_int.abs_eq)
>
> lift_definition foo45 :: "int => nat * nat" is "%(x,y). (nat x, nat y)"
>
> The last line gives this error:
>
> Lifting failed for the following types:
> Raw type: int
> Abstract type: nat
> Reason: No quotient type "Nat.nat" found.
>
> But my "foo45" represents what I want, but you'll have to tell me
> exactly what I have to do to get something like that.

The term "(nat x, nat y)" has type "int * int" and you want to lift it
to a term of the type "nat * nat". That's not possible because there is
not registered any such quotient (or subtype) (i.e., using integers to
represent natural numbers).

What you probably meant (but I don't know I am just guessing your
intentions), is this definition:

lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"

This is type correct but you can't prove the respectfulness theorem
since this theorem implies that each equivalence class in a definition
of integers contains exactly one element. That's not true.

You need some kind of a normalization function that picks up one element
for each class. For example:

lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" by auto

This gives you for each positive integer x a pair (x, 0) and for each
negative integer (0, 0).

For deep understanding I recommend read the paper that Brian and I wrote
about Lifting/Transfer and it is also good to know how typedef works.
You can also read a paper by Kaliszyk, Urban
(http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).

Ondrej

[Gottfried Barrow]

On 5/22/2013 1:58 AM, Johannes Hölzl wrote:
>> It'd be interesting to know if it's common these days for other
>> languages to use the classic definition of the integers as equivalence
>> classes like you did with Int.thy:
>>
>> https://en.wikipedia.org/wiki/Integer#Construction
>>
>> It seems it's common for the natural numbers to be built using the
>> successor function, but I'm guessing it's not so common for the integers
>> to be equivalence classes.
> In my experience it is quite the other way round. The first semesters
> mathematics course I attended introduced the integers, the rational
> numbers and the real numbers as equivalence classes. Only the natural
> numbers and the complex numbers where introduced like a datatype.

Johannes,

Thanks for your comment. I was comparing the formal, textbook
construction of the integers, as in what you're listing, to concrete
implementations of integers in programming languages, such as Coq,
Isabelle/HOL, Haskell, or any other language, old or new, but especially
new.

I'm speculating that this ability of Isabelle/HOL to define integers as
equivalence classes is special, and that it takes a special foundation
in a language to be able to do it, and that most languages don't have
the foundation to be able to do it in a practical way.

But I wouldn't know. This is the first time I've ever delved into the
low-level internals of a programming language, but defining an integer
as a set, in particular as an equivalence class, seems like it requires
some clever and sophisticated foundational code.

First, a person would simply know how it could be done at all. But
that's not enough; their code would have to perform reasonably fast.

I wouldn't know where to begin, and I'm sure any initial discovery of
mine on how to do it would be so slow, it would be useless.

All that to say, I'm guessing that Isabelle/HOL is pretty special in
this ability to achieve a textbook definition of the integers. But I try
not to become dogmatic about things I don't know about, and it could be
that it's very common for programming languages to implement integers as
equivalence classes.

Regards,
GB

[Lawrence Paulson]

Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.

Larry Paulson

[Christoph LANGE]

2013-05-22 14:26 Lawrence Paulson:

> Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.

Well, but there _is_ a notion of "programming" in Isabelle, given that
it is based on a functional programming language, isn't it? I recall
this earlier discussion on the title of the "programming and proving"
tutorial:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
Work-in-progress deadline 7 June; http://cicm-conference.org/2013/
→ OpenMath Workshop, 10 July, Bath, UK.
Submission deadline 7 June; http://cicm-conference.org/2013/openmath/

[Gottfried Barrow]

On 5/22/2013 8:26 AM, Lawrence Paulson wrote:
> Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.
>
> Larry Paulson

Larry,

My general rule is to never use emoticons, but rules have their exceptions.

You gave me that idea :). As to acronyms such as "lol", even under these
circumstances, they're still unacceptable.

This is the specific email:

http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00034.html

This will contain the thread:

http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html>

I was just starting to decide that under certain contexts, I could refer
to Isabelle/HOL as a programming language, because it's just a lot
easier to use that phrase sometimes, whereas, according to your specific
clarification in the email linked to above, Isabelle/Pure and
Isabelle/Isar are never to be called programming languages, so I try to
use "proof language" or "source language" when referring to them, even
when I know others might not get my point.

One of my other recent emails to the list spawned some private chatter
in which I referred to HOL as a programming language, which resulted in
a similar response to yours, which paraphrased would be, "What is this
programming language you're talking about in reference to HOL?"

That's why I had easy access to the links above, because I thought I had
the perfect, authoritative reference to explain that Isabelle/HOL is a
programming language, where Pure and Isar aren't.

In an attempt to use safe, correct vocabulary, I've resorted to using
"coding language" when trying to refer to the whole Isabelle family of
languages. At some point, there's a need for phrases, like, "I'm
programming with Isabelle/HOL", or, "I'm coding with Isabelle". Like I
say, "coding" has become my word of choice to replace "programming".

Anyway, I'm happy to try and use the official vocabulary correctly.
There are a ton of interwined languages with Isabelle, so I give up and
get lazy sometimes, and just say "programming language".

As to Coq, it seems to me if I can call Isabelle/HOL a programming
language, then I can call Coq a programming language. That's just an
aside. I'd be happy to use any official Coq vocabulary to use to refer
to Coq.

Regards,
GB

[Ramana Kumar]

On Wed, May 22, 2013 at 2:45 PM, Christoph LANGE <
math.sem...@gmail.com> wrote:

> 2013-05-22 14:26 Lawrence Paulson:
> > Coq and Isabelle/HOL are proof assistants, not programming languages. I
> can't imagine what gave you that idea. In Coq and Isabelle/HOL you write
> specifications, not code.
>
> Well, but there _is_ a notion of "programming" in Isabelle, given that
> it is based on a functional programming language, isn't it?

I would not put it that way.
Both Isabelle/HOL and <your favourite functional programming language> are
based on some flavour of lambda calculus. That's the connection.
However, there is no evaluation strategy specified for Isabelle/HOL terms,
and several constants don't have reducible definitions.
It's possible (and even common) to write uncomputable specifications in HOL
whereas you can't write anything uncomputable in a programming language.

[Lawrence Paulson]

You can call anything anything, but you are only complicating things for yourself. To my mind, asking why Isabelle/HOL has equivalence classes when Haskell doesn't and they are both programming languages is a bit like asking why a Boeing can fly and a Ford cannot when they are both cars.

Perhaps the term you are looking for is "formal language". Programming languages are formal, and higher-order logic is also a formal language. Just as Boeings and Fords are both vehicles.

Larry Paulson

On 22 May 2013, at 15:02, Gottfried Barrow <gottfrie...@gmx.com> wrote:

> On 5/22/2013 8:26 AM, Lawrence Paulson wrote:
>>
>> Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.
>>
>> Larry Paulson
>
> Larry,
>
> My general rule is to never use emoticons, but rules have their exceptions.
>
> You gave me that idea :). As to acronyms such as "lol", even under these circumstances, they're still unacceptable.
>
> This is the specific email:
>
> http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00034.html
>
> This will contain the thread:
>
> http://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/thread.html
>

[Gottfried Barrow]

Ondřej,

> What you probably meant (but I don't know I am just guessing your
> intentions), is this definition:
>
> lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"

Yes.

> This is type correct but you can't prove the respectfulness theorem
> since this theorem implies that each equivalence class in a definition
> of integers contains exactly one element. That's not true.
>
> You need some kind of a normalization function that picks up one
> element for each class. For example:
>
> lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" by
> auto

And so telling me that I need to prove "respectfulness" represents this
big need of people like me to have some understanding of what's going on
under the hood of the engine. Things like "fun" and lifting are great
because they take care of a lot of overhead, until I stray outside of
some example/template I have.

> This gives you for each positive integer x a pair (x, 0) and for each
> negative integer (0, 0).

This is one more time in which lifting appears to not be the best
solution. I think it'll be hard to beat the simple definition that I
came up with. But the value in these attempts to use lifting is in
getting closer to knowing what lifting is.

> For deep understanding I recommend read the paper that Brian and I
> wrote about Lifting/Transfer and it is also good to know how typedef
> works. You can also read a paper by Kaliszyk, Urban
> (http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).

And so I have 3 papers to pull from now, yours, Peter's and this one you
just listed. All along it's been, "Something's being lifted from
somewhere, to some thing, but what's being lifted is not clear to me,
and neither are the restrictions on what the some thing can be."

It looks like Urban and Kaliszyk's paper provides a good conceptual
overview. From section 5:/
/

/The main benefit of a quotient package is to lift automatically
theorems over raw types to theorems over quotient types. We will
perform this lifting in three phases, called regularization,
injection and cleaning according to procedures in Homeier’s ML-code./

So I was asking myself, "What's this Homeier's ML-code?"

And then I replied, "Oh, that would be Peter Homeier, who sent me a link
to his paper on quotients earlier in the day, in response to my global
request for docs on quotients and lifting."

With quotients and lifting, it appears that if you learn the one, you
learn the other.

Thanks,
GB

[Christian Sternagel]

Dear Gottfried,

my 2 cents concerning naming (everyone: please correct and/or complete):

- Coq is a proof assistant (or interactive theorem prover)

- Isabelle is a generic proof assistant, where Isabelle/HOL is its
instance for Higher-Order Logic. Thus I would call Isabelle/HOL a proof
assistant (omitting the term "generic"; also "interactive" from
"interactive theorem prover" is sometimes omitted, but I prefer not to
do so).

- The main purpose of proof assistants, as their name suggests, is to
assist the user to make proofs. That is, *proving* as opposed to
*programming* is the main thing.

- In the recent literature developing a theory (or a proof for some
statement) A in a proof assistant is called: mechanizing A, or
formalizing A, or certifying A, ... but never programming A

cheers

chris

[Gottfried Barrow]

Larry,

I was going to let your email be the end, a decision which actually
resulted in me culling out every point I thought about making, except
for trying to make a point with your transportation analogy.

To summarize the point to begin with, so you don't have to actually read
the analogy, it's just a variation of my past "Isabelle is awesome"
statements.

So Isabelle/HOL is a Boeing airplane, though a special model that's
configurable, and Haskell is a Ford car.

In regards to transportation, it appears not to make sense for a person
to make anything but the broadest of generalizations when comparing the two.

That's because, Isabelle, being a Boeing airplane, is certainly a means
of transportation, but the maintenance and fuel costs are extraordinary,
and so on the surface, to point out that Haskell, a Ford car, hasn't
implemented certain theoretical, engineering concepts when Isabelle has,
can appear to be dumb, especially, because practically speaking, as far
as transportation the advanced features are of no use.

However, the proper context is my use of the special, configurable
Boeing airplane. It happens to be that I have almost no interest in
traveling, I only care to theorize about traveling, in particular,
theorizing about air travel.

At this time, I don't have the money to even have the Boeing started up,
but then again, at this point, I only have a need to look at the Boeing,
and take a few measurements for certain parts that aren't completely
documented.

Now, I would hope that in several years, I'm doing something more than
what has already been done in regards to theorizing about air travel, to
the point to where I have a need to do more than just look at the
airplane, but in two years time, manufacturing costs being what they
are, there's some chance it will be affordable for me to pay some per
minute charge to reconfigure the special Boeing, where simply
reconfiguring it should answer some question I'll have.

So forth and so on. As times passes, what was once not affordable
becomes affordable, in regards to testing my theories. The upside is
that I may never have to resort to buying a Ford car, which is
accessible to the masses, but still costs a lot of money, and is a waste
if I don't have to do it.

And there's the possibility, if I can keep postponing the need for a
Ford car, that at some point, the configurable Boeing has ceased to be
leading edge technology, for near exclusive use by academics and
researchers, but the costs have dropped so much that it has become
commodity technology, and things have evolved for me to the where I now
have a need to travel, but not simply on the ground, like with the Ford
car, but in the air.

Do the designers intend for a person like me to use the Boeing in this
way? Probably not. Most likely, the configurable Boeing is meant as an
ends to a mean for professionals who work in the aerospace industry.

But instead of of using the configurable Boeing as an ends to a means, I
use it as an ends in itself, and because it can be used like that, it's
awesome.

Well, because I have no desire to ever work outside the realm of the
configurable Boeing, certain vocabulary doesn't fit my use of the Boeing
as good as it fits the designers use, but that idea is not to be pursued
here.

Regards,
GB

[Gottfried Barrow]

Christian,

There's no person on the face of the Earth more appropriate to continue
this conversation with than with you. So now, having intentionally tried
to make Larry suffer less, I now make you suffer.

There's a certain forum in which I deemphasized Isabelle as a
"programming language", a point which you countered, a counterpoint
which I partially countered.

As many times, what I reject, after having some time to think, I then,
in some form, embrace. And so, my mental investigations, even now, is in
trying to determine whether "programming language" can be legitimately
applied to Isabelle/HOL, where I'm leaning towards saying "yes", though
that doesn't mean I'll use the label anymore.

Having had my say with too many emails on this, I am now only interested
in choosing vocabulary for Isabelle for pure, practical reasons.

Without explaining any of the thought process that's led to this, I seek
one word, where the following describes some of the criteria:

1) What is one word which I can use to label the many languages that are
used in what I see in jEdit?

2) This word needs to general enough to describe the main languages that
I see: Pure, Isar, and Isabelle/HOL.

3) This word needs to be able to be used as a noun and a verb.

4) This word, as a noun, needs to describe what someone might want to
call me.

5) This word, as a verb, needs to describe I am doing when I use
Isabelle as a language.

6) This word needs to be acceptable by the experts as being technically
correct.

7) This words needs to have meaning to programmers who know nothing
about Isabelle as a language.

So the word "programming", because it's been used for years, and has
accumulated many connotations, doesn't work.

Below, you give me vocabulary, and I am happy to follow the lead of the
official documentation, the principal developers, and the rest of the
professional developers, like you.

But, as I said, my pursuit of a word is for everyday, practical usage.

To make a long story short, the word is "code".

Isabelle has source code files with the extension "thy".

1) If they are source code files, then what I'm looking at in jEdit must
be code.

2) If I'm editing code in a THY file, then it must be I'm coding.

3) If I ever get good enough at coding with the many languages of
Isabelle, then it must be that I'll be a "coder".

4) "Code" has no connotational requirement that anything be executed.

5) It doesn't have to be a recipe, as with programs.

6) "Code" is merely information that is "encoded".

So, at this point, seeing that "code", though commonly used, hasn't been
totally corrupted, maybe the proof assistant community can usurp the
word for their purposes.

Why? If leading authorities don't give the masses a practical word to
use for something, they'll choose their own word. Compare Latin to
Vulgar Latin. Language usage is heavily determined by anarchy.

Hypothetical scenario: I have 350 characters to make a comment on a
forum. Do I say, "When I myself am writing formal specifications with
Isabelle..."

Yes, I do, if I'm trying to be the benevolent educator, taking advantage
of what can be a teachable moment.

However, no, I don't, not if I'm at 400 characters. The phrase "writing
formal specifications with Isabelle" becomes "coding in Isa".

I've just mentioned an upside to the word "code". It's four letters. I
can't think of a three letter word at all to replace "code".

I'll check out of this thread on what is good or bad vocabulary.

Regards,
GB

[Walther Neuper]

On 05/23/2013 05:36 AM, Gottfried Barrow wrote:
>
> So the word "programming", because it's been used for years, and has
> accumulated many connotations, doesn't work.

> :

> To make a long story short, the word is "code".

Just saw another wording, "formalisation" in

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-May/msg00078.html
> For now I copied these into my formalisation. ...

"formalisation" is more specific and has a mathematical connotation,
which seems appropriate.

Walther

[Christian Sternagel]

I had that in my list too ... just saying ;) - cheers chris

[Makarius]

On Tue, 21 May 2013, Gottfried Barrow wrote:

> It'd be interesting to know if it's common these days for other languages to
> use the classic definition of the integers as equivalence classes like you
> did with Int.thy:
>
> https://en.wikipedia.org/wiki/Integer#Construction
>
> It seems it's common for the natural numbers to be built using the
> successor function, but I'm guessing it's not so common for the integers
> to be equivalence classes.

Here are some more Q&A threads on nat vs. int, and the natural
construction of int via quotients:

http://cstheory.stackexchange.com/questions/3772/why-naturals-instead-of-integers
http://mathoverflow.net/questions/29090/direct-construction-of-the-integers


Makarius

[Makarius]

On Wed, 22 May 2013, Lawrence Paulson wrote:

> Coq and Isabelle/HOL are proof assistants, not programming languages. I
> can't imagine what gave you that idea. In Coq and Isabelle/HOL you write
> specifications, not code.

I agree with that, although the "marketing" of proof assistants in the
last 10 years or so has moved in a different direction. Today most people
think of Coq as some dependently typed functional programming language,
and the Agda is emphasizing the programming aspect even more.

My own terminology is mainly about "formal languages" and "formalization"
of any kind. For example, the formal proof language of Isar is used to
write formal proofs, not to "program" nor to "implement" proofs.

Isabelle/ML and Isabelle/Scala happen to be programming languages just by
accident, so you can use them to program things. The Isabelle document
preparation language (formal latex) also happens to be computationally
complete, but nobody would say to "program" / "implement" / "code" some
text for a paper or book.


Interestingly, the computational or non-computational aspect of languages
often causes additional confusion for licensing. E.g. see the discussion
in the paper about "Licensing the Mizar Mathematical Library"
http://arxiv.org/abs/1107.3212

To my taste, the attempt to see Mizar articles as potentially
computational is even more artificial for that particular proof checker.


Makarius

[Makarius]

On Wed, 22 May 2013, Christoph LANGE wrote:

> Well, but there _is_ a notion of "programming" in Isabelle, given that
> it is based on a functional programming language, isn't it?

You need to be specific what you mean by "Isabelle". Maybe Isabelle/HOL?

In some sense, generic "Isabelle" is a framework (or playground) for a
multitude of formal languages of different use and purpose: Isabelle/ML,
Isabelle/Scala, Isabelle/Pure, Isabelle/HOL, Isabelle/Isar, Isabelle/XYZ.

See also
https://sites.google.com/site/isabelleedinburgh2013/Slides_makarius.pdf?attredirects=0
notably slide 4 about *some* languages of Isabelle.


Makarius

[Makarius]

On Wed, 22 May 2013, Gottfried Barrow wrote:

> 1) What is one word which I can use to label the many languages that are
> used in what I see in jEdit?

jEdit is a plain text editor. So you edit source text with it.

Isabelle/jEdit augments that a little bit to add formal markup from the
meaning of the source text right into the text view. This conforms to the
traditional notion of theory source text that you are editing, while the
prover is telling about the formal content of it.

Anyway, there is this old joke about "HTML as programming language". For
plain HTML 1/2/3/4 it was indeed a rather bad joke. For HTML5 I am not
sure anymore -- too many computational add-ons as it seems.


Makarius

[Lawrence Paulson]

If people want to prove theorems, they had better turn to us :-)

Larry

[Gottfried Barrow]

On 5/23/2013 6:32 AM, Makarius wrote:
> On Wed, 22 May 2013, Gottfried Barrow wrote:
>
>> 1) What is one word which I can use to label the many languages that
>> are used in what I see in jEdit?
>
> jEdit is a plain text editor. So you edit source text with it.

Makarius,

See, it's not like I'm wanting to rebel on the words I'm going to choose
to start referring to Isabelle, but my needs aren't the needs of 99.9%
of the people who use Isabelle, and I am a member of the masses who will
corrupt the language if given vocabulary that is too hard to use.

I can program some, but I'm not a programmer. There was a point at which
I would have been a programer who wrote diagnostic software for embedded
controllers, but that fell by the wayside.

The word "source" doesn't work in general.

1) In conversation, do I say, "The source on line 300 of Int.thy..."?
(That's not too bad.)

2) When I'm editing a THY, am I "sourcing"?

3) If I get good at using the languages of Isabelle, am I a "Isabelle
sourcer"? (Not to be confused with a sorcerer, one who works software
magic.)

I can try other words, like "specification", "formalize", and "proof".

1) "The specification on line 300 of Int.thy...".

2) "I myself, when specifying in Isabelle...".

3) "Someday, I might have earned the right to be called an Isabelle
specifier".

Will there come a day when I want to be called a "formalizer" or a
"prover"? Only if you take the lead and start calling yourself a
"formalizer" and a "prover" so that I have links to refer to when
someone says, "Uh, you're a formalizer, you say?"

In Isar, with my awareness raised, and because vocabulary used in
isar-ref.pdf, I can see that Isar is a "source language" in general, and
parts of it are a "proof language", so I've figured out the vocabulary I
need to use when referring to Isar.

However, it's not a simple thing to try and talk about the combination
of Isabelle/Pure, Isabelle/Isar, and Isabelle/HOL.

1) In a THY, you're always in Isar the source language, but from one
line to another, you may or may not be in Isar the proof language.

2) On a particular line, you are always in Isar the source language, but
your syntax may or may not be Isabelle/HOL syntax.

3) An outer syntax keyword may be both an Isar keyword and Isabelle/HOL
keyword, or it may only be an Isar keyword. One may need to look in
isar-ref.pdf for the characters "(HOL command)" to find out.

I suppose all this complexity is what gives Isabelle its power and
flexibility, but I'm talking about the need for the masses to engage in
polite conversation and not be saying things like, "You really should
try Isabelle, Joe. I've become an Isabelle specifier myself."

Regards,
GB

[Gottfried Barrow]

On 5/23/2013 6:32 AM, Makarius wrote:

> On Wed, 22 May 2013, Gottfried Barrow wrote:
>
>> 1) What is one word which I can use to label the many languages that
>> are used in what I see in jEdit?
>
> jEdit is a plain text editor. So you edit source text with it.
>

This email is one too many, other than I'd rather do this now, since the
thread has some momentum. Months from now, I don't want anyone to rehash
what's been said because I've decided to take the liberty to use
whatever vocabulary I want to use.

I'm settling on referring to Isabelle/HOL either as coding or as
programming, when I have a need to casually talk about it.

There's textbook style vocabulary that's used and being used in lots of
different places to label the languages of Isabelle, what Isabelle is,
and what you do when you're working with it. But I don't even see that
the developers are heavily using that type of language in day to day talk.

I'll take two words, "formalize" and "specification". To begin with,
they use too many characters. If you use "formalize", then you need to
use "formalization", which is even worse.

If I saw the Isabelle developers using these kind of words in the same
way that people talk about "programs" and "programming", then I suppose
I'd do it too, but am I suppose to look like a fool by heavily using
these formal sounding words when no one else has incorporated them into
their language similar to "program" and "programming"?

I'm willing to look the fool if there's a good reason, but I prefer to
minimize that kind of thing. And there's the huge issue of something
being practical. You can't expect me to have to use long, two word
phrases to refer to Isabelle code, or to refer to what I'm doing with
the Isabelle code.

This is not directed to anyone in particular, and my bi-monthly email
quota is up. You can blame Christian for badly influencing me.

Regards,
GB

[Makarius]

On Fri, 24 May 2013, Gottfried Barrow wrote:

> On 5/23/2013 6:32 AM, Makarius wrote:
>> On Wed, 22 May 2013, Gottfried Barrow wrote:
>>
>>> 1) What is one word which I can use to label the many languages that are
>>> used in what I see in jEdit?
>>
>> jEdit is a plain text editor. So you edit source text with it.
>

> The word "source" doesn't work in general.
>

> 2) When I'm editing a THY, am I "sourcing"?

You are a "writer" or "author" of formal source text, using a plain text
editor.

What is the terminology you would use yourself for latex sources? Latex
is also a programming language, but nobody "codes" papers, books, theses
etc. with it.

> I suppose all this complexity is what gives Isabelle its power and
> flexibility, but I'm talking about the need for the masses to engage in
> polite conversation and not be saying things like, "You really should
> try Isabelle, Joe. I've become an Isabelle specifier myself."

In the worst case, something like "user of Isabelle" will always work.


Makarius

[Gottfried Barrow]

On 5/24/2013 11:18 AM, Makarius wrote:
>
> You are a "writer" or "author" of formal source text, using a plain
> text editor.
>
> What is the terminology you would use yourself for latex sources?
> Latex is also a programming language, but nobody "codes" papers,
> books, theses etc. with it.
>

I don't think so Makarius. I'm still rebelling, and Larry has never
officially backed out of saying that Isabelle/HOL is a programming language.

There is "program", "programming", and "programmer", and "code",
"coding", and "coder", where right now I'm preferring "programming".

If someone asks, "What you do for a living?", do I say, "Well, I don't
get paid for it, but I'm a writer who writes writings."

Wouldn't they be more likely to say or think, "Oh, so you write novels,
or maybe you're a journalist?"

I am one over my bi-monthly quota of emails, but this is about the future.

Again, this is not directed at anyone in particular, but in the future,
if I'm corrected for using "programming" in relation to Isabelle/HOL, I
will reference the thread where Larry calls HOL a programming language,
and I will reference this thread.

I will then say, "then please give me three words to replace 'program',
'programming', and 'programmer'".

Me doing that will be much better than writing lengthy emails, as I have
been doing.

My goal is to become a very competent Isabelle/HOL "programmer". It's
the only "programming language" I use at this time. I do some scripting
and text processing, but there's already established vocabulary for
those, which would be "script" and "scripting", and "text" and "text
processing".

As a rebel, I can't see that it's reasonable for me to have to
frequently resort to long phrases like "I write formal source text".

Regards,
GB

[Gottfried Barrow]

On 5/24/2013 11:18 AM, Makarius wrote:

> In the worst case, something like "user of Isabelle" will always work.
>
> Makarius

So when the use of a language or product is prolific, such as with LaTeX
or Java, then using the name is enough to define what you do.

"What do you do?"

"I do Oracle."

If the use of Isabelle was prolific, then the use of "Isabelle/HOL"
would set the context. But Isabelle/HOL is relatively unknown in the
programming world, and it wouldn't solve my need for a word like
"programmer". Or maybe it would.

"What do you do?"

"I write HOL source."

But it's not prolific. So to say, "I write HOL source", is to invite the
question, "Oh, that sounds interesting. But what is that exactly?"

Instead of,

"What do you do?"

"I'm a programmer."

"Oh." (Their eyes shift around, looking for someone else to talk to.
That's good. You didn't feel like talking about it either.)

Regards,
GB