Re: [isabelle] Isabelle functions: Always total, sometimes undefined



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
Description: OpenPGP digital signature



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