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