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
Introduction
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.
Background
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$}
Conclusion
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".