Re: [isabelle] Infinitely recursive lambda expression or not?



This document seems a good introduction on LCF vs HOL and the idea of getting one with the other:
http://csep.hpcc.nectec.or.th/Journals/oup/smj/journals/ed/titles/computer_journal/Volume_38/Issue_02/38.2.pdf/agerholm.pdf
(the one I will read)

For HOL and LCF as an Isabelle theory, this one:
http://www4.in.tum.de/publ/papers/Regensburger_HOLT1995.pdf
(outdated?)

Quote of the abstract of the former:

The LCF theorem prover provides a logic of domain theory and is useful for reasoning about nontermination, general recursive definitions and infinite-valued datatypes like lazy lists. Because of the continued presence of bottom (undefined) elements, it is clumsy for reasoning about finite-valued datatypes and strict func- tions. By contrast, the HOL theorem prover provides a logic of set theory (without a notion of undefinedness) and supports reasoning about finite-valued datatypes
and primitive recursive functions well.

I was not suspecting this kind of difference between HOL and LCF provers and their logics.

On Fri, 27 Dec 2013 18:50:26 +0100, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

You could try Isabelle/HOLCF, but I’m not sure how well documented and supported it is.

Larry Paulson


On 27 Dec 2013, at 17:47, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:

Le Fri, 27 Dec 2013 18:33:49 +0100, Lawrence Paulson <lp15 at cam.ac.uk> a écrit:

From a computational point of view, "f a = (a ∨ f a)” must be regarded as undefined, because the recursion is not well-founded. There are logics where you could then prove that f(True)=True and f(False)=undefined.

Larry Paulson


Interesting. Just out of curiosity and learn more (really not to use it), what are the names of these logics?


--
“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.