The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Quite a lot of cool, if I might say so.

I've only have a quick glimpse at the proof. Let me try to summarise my understanding of it: you prove to each total recursive function (in the sense that its graph is a total functional relation) then there corresponds a normalisable lambda-term (in the sense of the accessibility predicate) and then you define a function by recursion over this accessibility predicate.

Is that correct?

This makes use of the singleton-elimination of accessibility. A subtle point in Coq (in particular since it's hard to reconcile with judgemental proof irrelevance, and this is an extension of Coq which has been mooted a number of times). For instance, you mention that if totality of the recursive function is proved with axioms, then a Coq function still emerges. This would be right, but I'd expect the function to block on some natural numbers as it would need to match on the axioms.

On 2 February 2017 at 16:18, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Dear Coq users,

I am happy to announce the availability of a dependently typed
implementation of the untyped Lambda Calculus in Coq.

http://www.loria.fr/~larchey/Lambda_Calculus

One of the by-products of that development is a formal proof
that:

Every total recursive function f : N -> N can be represented by
Coq term tf : nat -> nat (which can be computed from the algorithm
that describes f.) (*)

Of course the problem is to circumvent the unbounded minimization
scheme. I know that there have been many published (and unpublished)
implementations of the untyped Lambda Calculus.

This one enjoys the following properties:

1/ A dependently typed representation of terms which avoids the problem
   induced by alpha conversion: two alpha-equivalent terms are equal.
   The type of terms is parametrized by the number of usable free
   variables.

2/ Most of the proofs of JL Krivine's book "Lambda-Calculus: Types and
   Models" are implemented in an intuitionistic way (no axiom is used).
   Intersection types system D and Domega are implemented with the
   characterization of strongly normalizable terms.

   System F is not implemented yet though (but this is not really
   the goal of this project).

3/ A dependently typed representation of recursive algorithm and
   a formal proof of the encoding of recursive algorithm by untyped
   lambda terms.

The main objective of this project is to build a Coq library
that could be used to implement *undecidability results*
(for various logics) in an intuitionistic way.

The development is ongoing on my private repository but anyone
interested in such a project can be given access to that
development branch. Do not hesitate to contact me.

Dominique Larchey-Wendling
TYPES, LORIA, CNRS

(*) the word "total" which could be ambiguous (as it refers to
meta-theory), should here be understood as "provably total" in Coq