*To*: "Lawrence Paulson" <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Yannick <yannick_duchene at yahoo.fr>*Date*: Fri, 27 Dec 2013 23:52:19 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <96B664CD-843C-40AE-A880-4B08F36B1207@cam.ac.uk>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <52AC4D87.9030304@gmx.com> <op.w723lrn9ule2fv@cardamome> <52B227C7.6070607@gmx.com> <op.w8p2ilo1ule2fv@cardamome> <op.w8rgogrkule2fv@cardamome> <2D976E64-08BA-4145-ACC3-588AFC48DF66@cam.ac.uk> <op.w8rid9n7ule2fv@cardamome> <96B664CD-843C-40AE-A880-4B08F36B1207@cam.ac.uk>*Reply-to*: yannick_duchene at yahoo.fr*User-agent*: Opera Mail/12.16 (Linux)

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 usefulforreasoning about nontermination, general recursive definitions andinfinite-valueddatatypes like lazy lists. Because of the continued presence of bottom(undefined)elements, it is clumsy for reasoning about finite-valued datatypes andstrict func-tions. By contrast, the HOL theorem prover provides a logic of settheory (withouta notion of undefinedness) and supports reasoning about finite-valueddatatypesand primitive recursive functions well.

You could try Isabelle/HOLCF, but I’m not sure how well documented andsupported it is.Larry PaulsonOn 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 regardedas undefined, because the recursion is not well-founded. There arelogics where you could then prove that f(True)=True andf(False)=undefined.Larry PaulsonInteresting. Just out of curiosity and learn more (really not to useit), 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

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Lawrence Paulson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Date: [isabelle] A problem on ML-like function programming
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: [isabelle] Hide all constructors of a datatype automatically
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list