# 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.*