Email Gateway (Aug 22 2022 at 08:59): Email Gateway (Aug 22 2022 at 08:59):From: Larry Paulson <lp15@cam.ac.uk>
Note that I am moving your question to the Isabelle Users’ mailing list.
It would be helpful if you would say which document refers to 3 levels of lambda calculus. As you note, this is incorrect and needs to be reworded. Isabelle/HOL does provide two levels of logic; a question on that topic was answered within the past month. (And we have a FAQ here: https://isabelle.in.tum.de/community/FAQ)
Larry Paulson
Email Gateway (Aug 22 2022 at 09:00):From: Larry Paulson <lp15@cam.ac.uk>
I think your clue here is the phrase "type-theoretic parlance”, which is to say that people from that background may want to see ==> as a function type, for example, analogously to LF, which can be regarded as the type-theoretic analogue of Isabelle Pure.
Larry Paulson
Email Gateway (Aug 22 2022 at 09:01):From: Askar Safin <safinaskar@mail.ru>
Thanks for answer. The document is isar-ref from isabelle 2013. Exact text is "The Pure logic [38, 39] is an intuitionistic fragment of higher-order logic[13]. In type-theoretic parlance, there are three levels of λ-calculus with corresponding arrows =>/\<And>/==>".
Also, FAQ doesn't say about levels of lambda calculi.
==
Askar Safin
http://vk.com/safinaskar
Kazan, Russia
Email Gateway (Aug 22 2022 at 09:01):From: Makarius <makarius@sketis.net>
On Tue, 3 Mar 2015, Larry Paulson wrote:
I think your clue here is the phrase "type-theoretic parlance”, which is
to say that people from that background may want to see ==> as a
function type, for example, analogously to LF, which can be regarded as
the type-theoretic analogue of Isabelle Pure.
Yes, this text in the "isar-ref" manual (section 2.1) and a slightly
longer version in the "implementation" manual (chapter 2) emerged from
what I've learned from people in Edinburgh, Cambridge, Nijmegen, and
especially Stefan Berghofer in Munich around 2000. It is an attempt to
explain things in a way that everybody understands, both
strongly-dependent types and classic logicians.
On 3 Mar 2015, at 12:48, Askar Safin <safinaskar@mail.ru> wrote:
The document is isar-ref from isabelle 2013.
By the default, you should use the current official release for
everything, including the continously growing/updated manuals. Presently
it is Isabelle2014 (August 2014).
Also, FAQ doesn't say about levels of lambda calculi.
Before Larry mentioned that, I hardly remembered this ancient relic at
all. Apart from the isabelle-users mailing list, the current Q&A platform
is Stackoverflow: http://stackoverflow.com/questions/tagged/isabelle
You should quickly get some idea who is active where, and which kind of
discussions or question/answer threads are better place on this site or
that site.
Makarius
Email Gateway (Aug 22 2022 at 09:04):From: Askar Safin <safinaskar@mail.ru>
That text about 3 levels still present at http://isabelle.in.tum.de/dist/Isabelle/doc/implementation.pdf :
"Following type-theoretic parlance, the Pure logic consists of three levels of λ-calculus with corresponding arrows"
"Thus all three levels of λ-calculus become explicit"
"On top of these syntactic terms, two more layers of λ-calculus are added"
There may be other occuriencies.
Also, http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf says:
"In type-theoretic parlance, there are three levels of λ-calculus with corresponding arrows"
And I would suggest "grep" current development repo of Isabelle for "3 levels", "three levels" and similar :)
Also, some more bugs in docs (in that online versions):
implementation.pdf, "As in regular typography, there is some extra space before section headings
that are adjacent to plain text, bit not other headings as in the example
above", seems "but" should be instead of "bit"
implementation.pdf, "The next example shows how to embed ML into Isar proofs, using ML_prf
instead of Instead of ML"
==
Askar Safin
http://vk.com/safinaskar
Kazan, Russia
Email Gateway (Aug 22 2022 at 09:04):From: Makarius <makarius@sketis.net>
On Fri, 6 Mar 2015, Askar Safin wrote:
That text about 3 levels still present at http://isabelle.in.tum.de/dist/Isabelle/doc/implementation.pdf :
"Following type-theoretic parlance, the Pure logic consists of three levels of λ-calculus with corresponding arrows"
"Thus all three levels of λ-calculus become explicit"
"On top of these syntactic terms, two more layers of λ-calculus are added"
There may be other occuriencies.Also, http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf says:
"In type-theoretic parlance, there are three levels of λ-calculus with corresponding arrows"And I would suggest "grep" current development repo of Isabelle for "3 levels", "three levels" and similar :)
I don't see anything wrong here. What do you mean exactly?
Side-remark: the best way to "grep" through Isabelle sources these days is
via hypersearch in Isabelle/jEdit. It is one of the big assets of the
underlying jEdit text editor.
Also, some more bugs in docs (in that online versions): * implementation.pdf, p. 74, figure 2.3 after footnote
I think this is the normal way of Don Knuth and/or Leslie Lamport
typesetting floating boxes.
- implementation.pdf, "As in regular typography, there is some extra space before section headings
that are adjacent to plain text, bit not other headings as in the example
above", seems "but" should be instead of "bit"- implementation.pdf, "The next example shows how to embed ML into Isar proofs, using ML_prf
instead of Instead of ML"
I am going to change the "bit" in to "but" and remove the extra "Instead
of".
Makarius
Email Gateway (Aug 22 2022 at 09:05):From: Makarius <makarius@sketis.net>
(This is bounced back to isabelle-users. Discussions on mailing lists
should not be downgraded into private threads, especially with other
people on the original thread.)
On Fri, 6 Mar 2015, Askar Safin wrote:
I don't see anything wrong here. What do you mean exactly?
Larry just said that there is really 2 levels of lambda calculi and not
3. And I agree :) Because we have two kinds of things which can be
lambdas - it is terms (with normal types as types of this terms, with
normal lambdas %, with normal application as application, with arrow =>
for construction of function types) and proofs (with propositions as
types of this proofs, with "assume" and "fix" as lambdas, with
meta-modus-ponens as application, with arrows ==> and \<And> [yes, now I
understand that!] for construction of function types). Yes, we have 3
lambda constructors: "%", "assume" and "fix" with corresponding arrows
=>, ==> and \<And>. But we have only two kinds of things which support
this lambdas: it is terms and proofs.
Larry first thought the subject refers to the "meta-logic" (Isabelle/Pure)
versus "object-logic" (Isabelle/HOL).
The pieces of text under discussion refer to the structure of
Isabelle/Pure itself, in a way that hopefully people with type-theory
background will recognize. Thus it is meant to bridge over cultural gap
of various proof-assistant communities. When talking to type-theory guys,
they could usually follow my explanations, although I am not an expert on
that subject myself. (If some type-theory expert points out mistakes in
the text, I will listen carefully.)
To understand the business of levels of lambda calculus better, you can
either study the cited material [1] (Barendregt, Geuvers) or [2]
(Berghofer, Nipkow) -- according to the bibliography in the
"implementation" manual.
If you don't care about type-theory, you can ignore all that, and merely
observe that there is always something left that one does not know --
according to best scientific principles.
I think this is the normal way of Don Knuth and/or Leslie Lamport
typesetting floating boxes.
This is ugly. Please, fix this somehow, even using some hacks.
I count the words "bug", "fix", "hack" as street language. Something not
to be done in educated circles of formal logic.
If you can provide a proof that I am using LaTeX in a bad way (which is
quite possible), I will change that. If you can provide a proof that
Knuth/Lamport did something fundamentally wrong, it can be discussed.
One needs to avoid acting erratically out of ignorance, though.
Makarius
Email Gateway (Aug 22 2022 at 09:05):From: Makarius <makarius@sketis.net>
Yes, and most of that is of quite low quality.
Makarius
Email Gateway (Aug 22 2022 at 09:05):From: Askar Safin <safinaskar@mail.ru>
(This is bounced back to isabelle-users. Discussions on mailing lists
should not be downgraded into private threads, especially with other
people on the original thread.)
Sorry, I ocassionally typed "Reply" instead of "Reply to all"
Larry first thought the subject refers to the "meta-logic" (Isabelle/Pure)
versus "object-logic" (Isabelle/HOL).
I mean meta-logic, too.
I count the words "bug", "fix", "hack" as street language. Something not
to be done in educated circles of formal logic.
This is normal words in programming world, including free software. You can see them often in docs and mailing lists for free software.
==
Askar Safin
http://vk.com/safinaskar
Kazan, Russia
Email Gateway (Aug 22 2022 at 09:06):From: Makarius <makarius@sketis.net>
Someone has pointed out the "footmisc" package by private mail.
There is also a related discussion on Stackoverflow
http://tex.stackexchange.com/questions/32951/tables-below-footnotes-is-this-a-good-output-routine-algorithm-or-a-bug
with some interesting answers.
Someone over there just said "You can fix this by the footmisc package."
without any explanation nor discussion why it is wrong and why the other
behaviour is less wrong.
Someone else has a more subtle discussion, and puts dangerous words like
"bug" or "feature" in quotes, as I usually do myself.
Makarius
Email Gateway (Aug 22 2022 at 09:06):From: Askar Safin <safinaskar@mail.ru>
Of course, putting footnotes after figures is wrong. Because on would search footnotes in the bottom of page.
Email Gateway (Aug 22 2022 at 09:06):From: Makarius <makarius@sketis.net>
Maybe you want to join the discussion at
http://tex.stackexchange.com/questions/32951/tables-below-footnotes-is-this-a-good-output-routine-algorithm-or-a-bug
which is the place for TeX/LaTeX experts.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC