Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on April 7th 2016

Personnes présentes

  • Thibaut Balabonski
  • Frédéric Boulanger
  • Yakoub Nemouchi
  • Safouan Taha
  • Burkhart Wolff
  • Lina Ye

Candidats de Réductibilité en Nominals

Presentateur: Benoit Valiron


Benoit is presenting the “Candidats de Reducibiité en Nominals” in the Isabelle Nominals-Package. The talk is in the continuity of an introductory talk on the same subject.


Benoit proceeds as follows:

  • Repetition of the basic concepts Nominals and its implementation in Isabelle. See the excellent slides of A. Pitts.
  • Crash Course on typed lambda calculus
    • {$\lambda$}-terms: {$t ::= \lambda x. t ~|~ t\,t ~|~ x$}
    • (simple) types: {$A ::= \alpha ~|~ A \Rightarrow A$}
    • type judgements : {$x_1 : A_1, … , x_n : A_n \vdash T : B$}
    • introduction of classic inductive definition of well-typed type judgements.
  • Re-introduction of classic notions of executability: {$\beta$} - reduction , {$\alpha$} - congruence.

Discussion of specific Isabelle/Nominal constructs:

  • nominal_inductive
  • nominal_primrec

which allow to define the “classical” definitions of well-typedness and recursion on the equivalence

Proof of Termination of Simple-typed Lambda via "Candidats of Reducibility".

  • {$RED_A$} : set of converging terms of type A.
  • {$RED_{\alpha} = \{ t. t \in SN \wedge \vdash t : \alpha \}$}
  • {$RED_{A\Rightarrow B} = \{t. t : A \Rightarrow B \wedge \forall u. u \in RED_A \Longrightarrow t u \in RED_B\}$}

Defining a critical invariant (the key-issue):

  • CR1 : {$t \in RED_A \Longrightarrow t \in SN$}
  • CR2 : {$t \in RED_A \wedge t \to t’ \Longrightarrow t’ \in RED_A$}
  • CR3 : {$t$} is neutral (i.e. not a lambda-abstraction) {$\Longrightarrow (\forall t’. t \to t’ \Longrightarrow t’ \in RED_A \Longrightarrow t \in RED_A) \Longrightarrow t\in RED_A$}

Induction yields Theorem : {$\vdash t : A \Longrightarrow t \in RED_A$}


The underlying question is: Is the Nominals-Package is actually suited to tackle "hard" problems on the meta-theory of the typed $\lambda$-calculus ? Could it be a true alternative for a model of "Isabelle/Pure" ?

A short first answer to the first question clearly is : "yes". The presented example is challenging and yet part of the standard example suite. However, effective working with the package requires knowledge about another layer of tactics and infrastructure over Isabelle, about whose power not very much is known. So, the answer to the second question is so far : "Don't know".

Previous meeting -- Next meeting