Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?



An attempt to draw a picture of what various meanings of HOL may be, was already made in a prior thread in this news‑group (last year, I believe), and it's indeed rather large, especially for a non‑student/non‑professional.

What I understand from the second paper, is that the “λ” in “λHOL” denotes a reference to the location of the named theory on the lambada‑cube (something I already heard about before).

I had this question wondering if it's something new I did not knew or a new name for something I already knew. To tell more, my guess is: HOL is a friendly name, and λHOL is a more formal name with a reference to the lambda‑cube, so not a new logic (if I'm not wrong).

With thanks for your concern

On Tue, 30 Sep 2014 09:17:21 +0200, Ramana Kumar <rk436 at cam.ac.uk> wrote:

You might want confirmation from more than one author on this, or at least someone who isn't primarily using dependently >typed systems. Certainly I find the sentence you quoted from the abstract of the first paper confusing. But there are many >variations on what is called "HOL"; it would be nice to find a paper that does a comprehensive summary and comparison.

On Tue, Sep 30, 2014 at 4:38 AM, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
I guess I found an answer here, http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers_sl3.pdf , and the >>answer is yes.

Le Mon, 29 Sep 2014 05:51:53 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:


Hi all,

I'm not playing with Isabelle since some time, but still read from time to time on things around it: type theory and >>>proof theory and HOL. I came to a question related to HOL and type theory, and though this may be the best place to ask >>>for, due to Isabelle being very close to it.

I landed onto this paper: http://www.cs.ru.nl/~herman/PUBS/inconsist-hol.pdf

In the abstract, it says “HOL, or its type theoretic variant λHOL”. Does that mean the real name of HOL with simple >>>type theory is λHOL? And also, does that mean there exist(ed) an HOL outside any type theory? (for the latter, I don't >>>see how, but may be I'm too much biased on this). Or I am misunderstanding this sentence?


With thanks, and have a nice day.




--“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






--
Yannick Duchêne


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