*To*: Joachim Breitner <joachim at cis.upenn.edu>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Isabelle functions: Always total, sometimes undefined*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 19 Oct 2017 11:30:33 +0200*In-reply-to*: <1507832320.1851.4.camel@cis.upenn.edu>*Organization*: TU Munich*References*: <1507832320.1851.4.camel@cis.upenn.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0

Hi Joachim, > based on repeated discussions and confusion when interacting with> functional programmers and type-theory based theorem prover users, I> wrote a blog post explaining how functions in Isabelle are different> than functions in Haskell/Coq/etc, and what the deal is about> undefined:> > http://www.joachim-breitner.de/blog/732> > Please let me know if I say something wrong that should not be said> like that on the Internet. Otherwise, feel free to share when you have> trouble explaining these things to someone. thanks for that blog post, which does indeed cover the essence of the relationship of Isabelle/HOL and functional programming. Let me add some remarks: a) Terminology You are mixing Isabelle and Isabelle/HOL quite freely. IMHO it should read Isabelle/HOL throughout. b) Section ÂNot all function specifications are okÂ Notation ÂSÂ stands beside ÂSucÂ. You might want to consolidate that. c) Section ÂYou can still compute with Isabelle functionsÂ You might want to add the key idea of the âmoral reasoningâ foundation: interpret HOL equations as a *shallow embedding* of corresponding programs. The approach still has its advantages, e.g. you get datatype abstraction (almost) for free. Lars' work goes beyond that by constructing a *deep embedding* of equations into HOL itself. d) Section ÂTermination is a property of specifications, not functionsÂ Speaking about ÂterminationÂ for function specifications is illusive, since the logic itself does not know about a concept called ÂterminationÂ. But you can utilize typical termination arguments (e.g. well-founded relations) to automate the derivation of equations from a primitive, abstract definition. e) Why there is nothing but a quite loose characterization of the ÂexecutableÂ sublanguage of Isabelle/HOL. It is the sheer complexity of the system itself: The sublanguage is not built into the logic, but appears by a elaborate stack of tools: * Tools to introduce concepts known from FP in a suitable manner: datatype, function. * Tool to generate programs for sets of equations: code generator. Both layers are highly customizable. Of course you can do some kind of FP while you use, but you are always free to make it crumble down doing some â apparent according to common sense but difficult to characterize precisely â ÂnonsenseÂ, e.g. non-terminating simp rules for the termination prover. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Isabelle functions: Always total, sometimes undefined***From:*Lawrence Paulson

**References**:**[isabelle] Isabelle functions: Always total, sometimes undefined***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Performing global rewrites on the code setup
- Next by Date: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Previous by Thread: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Next by Thread: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Cl-isabelle-users October 2017 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