The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

Hi,

>   But then I get the error message:
> Error: Non strictly positive occurrence of "_UNBOUNDED_REL_?" in ...
>
>   Can anybody explain me why this inductive definition is not 
> well-formed

Coq rejects this kind of definitions, because one could use it to write 
non-normalizing terms, for example by embedding the pure 
lambda-calculus:

Inductive Term : Set :=
  Lambda : (Term -> Term) -> Term.

Definition App (t u : Term) : Term :=
  match t with Lambda f => f u end.

Definition omega := Lambda (fun x => App x x).

Now you get the well-known infinite reduction chain
  App omega omega
-> (fun x => App x x) omega
-> App omega omega
-> ...

Since terms can appear in types this would make it impossible to decide 
if, e.g., an application is well-typed.
Another question: Is there any damage apart from this? Would it be 
consistent?

best,

Roland