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:
(the one I will read)
For HOL and LCF as an Isabelle theory, this one:
Quote of the abstract of the former:
The LCF theorem prover provides a logic of domain theory and is useful
reasoning about nontermination, general recursive definitions and
datatypes like lazy lists. Because of the continued presence of bottom
elements, it is clumsy for reasoning about finite-valued datatypes and
tions. By contrast, the HOL theorem prover provides a logic of set
a notion of undefinedness) and supports reasoning about finite-valued
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>
You could try Isabelle/HOLCF, but I’m not sure how well documented and
supported it is.
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
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
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and