Re: [isabelle] Non terminating function proven terminating



On Fri, 21 Oct 2011, gallais @ ensl.org wrote:

Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle. As in Agda, we do not lose SN but we do accept a function that is not well-defined.

fun f :: "unit \<Rightarrow> unit" where
 "f x = (\<lambda> _ .  ()) (f ())"

lemma fail : "f () \<equiv> ()"
by simp

You quote this like something that is well-known in the constructive community. Can you point to some mailing list threads discussing it, or similar?

On his web page, Pierre Boutillier has the following interesting quotation:

  What I cannot create, I do not understand.
  Richard Feynman (Merci O. Danvy)

This attitude might explain part of the confusion. Isabelle/HOL is a very platonistic system, using classical mathematical principles that are not as "created" as one would expect in Coq or Agda.

As Tobias has already pointed out, our abstract syntax layer works modulo
various reductions (alpha, beta, eta) that are considered a purely syntactic device on the term language, without any computational idea behind it. The heavy lifting is then done in classic set-theory of HOL behind the scenes, so that the original specification of the user is eventually derived as actual theorems (plus extra infrastructure such as simplification and induction rules).


Back to the example:

  fun f :: "unit => unit" where ...

My first reaction as a classically-mindend person: Isn't there just one such function "unit => unit", namely "\<lambda>x. ()", so it does not really matter what the user specifies or the system defines behind the scenes, the "fail" result always holds universally:

lemma
  fixes f :: "unit \<Rightarrow> unit"
  shows "f x = ()" by (cases "f x")

But the unit type is not really essential in the "trick". Consider this variant:

fun g :: "'a \<Rightarrow> 'a" where
  "g x = (\<lambda>_. undefined) (g undefined)"

Here "undefined" is just a global unspecified constant that is used as a dummy here. Equally well you could have written this from the very start:

fun g :: "'a \<Rightarrow> 'a" where
  "g x = undefined"

Here we know that "g x" is always that constant, without known what it is. (It might also depend on the type 'a.) The Isabelle/HOL library has a slightly more constructive variant of this idea, where some overloaded constant "default" is the parameter of a type-class of the same name. Thus the value is usually known from the type structure by extra-logical means, such that the code generator can use that information, for example.


	Makarius





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