The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Wed, 11 May 2005, Adam Koprowski wrote:

>    Dear all,
>   I'm trying to formalize computability property on terms of simply-typed
> lambda calculus. Definition is as follows:
>
> Def. Computability: A simply-typed lambda term s is computable iff
> (i) s is of atomic type and s is strongly normalizable, or
> (ii) s is of arrow type A -> B and @(s, t) is computable for every
> computable term t: A
>

As you mention in your title, defining Computability as an inductive
predicate implies a non-strictly positive occurence, that Coq will not
allow. By the way, the _UNBOUND_REL_ is a bug, it shouldn't appear.

Nevertheless, you can define this Computability predicate in Coq, but as a
function rather than as an inductive:

Fixpoint SC (rho:type)(r:term) {struct rho} : Type :=
  match rho with
   | Iota => SN Iota r
   | Arrow rho sigma => forall s:term, SC rho s -> SC sigma (App r s)
  end.

This is a simplified excerpt taken from a formalization of a normalization
proof a la Tait due to U. Berger that I've just finished in Munich, in
cooperation with H. Schwichtenberg. The files of this formalization are
accessible at http://www.lri.fr/~letouzey/download/tait.tgz, and the SC
predicate is in TaitCore.v. We are currently working on an article
describing this work, but in the meantime you can find a couple of pages
describing briefly this SC in a paper submitted to TYPES:
http://www.lri.fr/~letouzey/download/Letouzey_Spitters_05.pdf

Best regards,
Pierre Letouzey