Objectif : intégrer fold/unfold dans Dedukti

Avec des règles de réécriture du genre : Nat(n) -> ... Nat(m)... le typechecker boucle.
Une solution, adoptée par lemuridae, est de séparer les règles de réécriture en deux ensembles : le premier modulo lequel le système de type est considéré, le second contenant des règles destinées à être pliée/dépliées explicitement. Il faut donc prévoir deux nouvelles constructions dans les termes de preuves et les règles de typage et de réduction qui vont avec. Pour la règle de réécriture R : P -> Phi, on a les deux règles de typage suivantes :


pi : Phi
-------------- (pliage)
R pi : P


pi : P
--------------------------- (dépliage)
let (R x) = pi in x : Phi


et la règle de réduction :

let (R x) = R pi in x --> pi


On ne peut pas s'en passer dans lemu car on n'a pas de règles de réécriture sur les termes de preuve, seulement sur les termes du premier ordre. En revanche, on peut réécrire les termes de preuve dans Dedukti, donc on peut simuler
fold/unfold avec deux axiomes et une regle de réécriture:

foldR : x1:T1 -> ... -> xn:Tn -> Phi:Prop -> P
unfoldR : x1:T1 -> ... -> xn:Tn -> P:Prop -> Phi

et la règle

unfoldR (foldR pi) --> pi

On perd juste un peu le confort apporté par l'instanciation automatique de x1 ... xn lors de l'application des règles d'inférence.

Un fichier arith.eu a été créé dans les exemples de Deduktipour démontrer la faisabilité de cette "technique".

Reste du séjour

Correction de bugs divers et avancement dans la traduction du prélude de Coq.