The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

On Wed, 11 May 2005, Roland Zumkeller wrote:

> 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?

with a constructor whose argument is a predicate, you may have trouble:
(it's inspired from page 50 in 
http://www.lix.polytechnique.fr/~dowek/Publi/habilitation.ps.gz)

take * = Prop

take c:(I=>*)=>I, F:I=>(I=>*) and assume that F(cX) -> X

the existence of c means that F is surjective: there is no more subsets of I 
than there is elements in I!...

take P = [x:I]~(Fxx) : I=>*  (~:(X:*)X=>False)

t = cP : I and Q = Pt : *

then Q = Pt -> ~Ftt = ~F(cP)t -> ~Pt = ~Q -> ...

so, Q = ~Q

now, take u = [x:Q]xx : ~Q

then, uu : False