coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] guarded recursion and termination

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
Cc: Gert Smolka <smolka AT ps.uni-saarland.de>, coq-club AT inria.fr
Subject: Re: [Coq-Club] guarded recursion and termination
Date: Sun, 19 Sep 2010 09:10:39 -0400

> Martin-Loef''s W-type is universal for strictly positive definitions. I am
> not sure when W-types appeared first, they certainly feature in the 1980
> Sambin/Martin-Loef book.

I am not sure that it is entirely correct since "strictly positive"
definitions also include things such as the definition of the identity types
which (as far as I know) can not be encoded through W-types.

Vladimir.

[Coq-Club] guarded recursion and termination, Gert Smolka
- Re: [Coq-Club] guarded recursion and termination, Pierre Casteran
  - Re: [Coq-Club] guarded recursion and termination, Gert Smolka
    - Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
      - Re: [Coq-Club] guarded recursion and termination, Vladimir Voevodsky
        
        Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
      - Re: [Coq-Club] guarded recursion and termination, Gert Smolka
    - Re: [Coq-Club] guarded recursion and termination, Pierre Casteran
- Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
- Re: [Coq-Club] guarded recursion and termination, Pierre Casteran