Sur le problème de la décision pour le lambda-calcul typé avec des coproduits

Martin Hofmann

Travail conjoint avec:

T. Altenkirch, Univ. of Munich, Germany P. Dybjer, Chalmers University, Sweden P. Scott, Univ. of Ottawa, Canada.

Nous considérons le problème de la décision pour le lambda-calcul simplement typé avec le coproduit (réunion disjointe) de types engendré par un type de base [BASIQUE?]. C’est-à-dire, on rajoute au lambda-calcul typé avec un type basique [??] une opération de formation de types A + B, et les termes suivants:

inl(t) : A + B, when t : A
inr(t) : A + B, when t : B
case(t_{1}, t_{2}, t_{3}) : C, when t_{1} : A + B, t_{2} : A→C, t_{3} : B→C

Deux termes sont équivalents sémantiquement s’ils ont la même dénotation dans l’interpretation ensembliste évidente consistant à interpréter le type de base comme un ensemble infini et le coproduit comme la réunion disjointe.

Par exemple, nous avons l’équivalence:

case(x, λx.y, λx.y) = y

et, plus généralement, si t_{1} = t_{2}, alors,

case(x, λx.t_{1}, λx.t_{2}) = t_{1}(= t2)

pourvu que t_{1}, t_{2} ne contiennent pas x.

Dougherty et Subrahmanyam (1995) ont montré que l’équivalence sémantique est reflétée par la théorie équationnelle naturelle (BiCCC) obtenue à partir de la théorie des catégories bicartesiennes fermées.

Un problème ouvert de longue date est de donner un procédé de décision effectif pour cette théorie BiCCC. On obtient une solution basée sur la technique de normalisation par évaluation (NBE) introduite par Schwichtenberg et Berger (1991) et rafinée par les auteurs en utilisant des méthodes de la théorie des catégories.

Nous utilisons NBE pour associer des formes normales à des termes. Une égalité non triviale entre formes normales est alor décidée en utilisant un système de preuves basé sur les tableaux. Les principaux résultats techniques ici sont l’admissibilité de la transitivité (correspondant à l’élimination des coupures) et la détection de branches infinies.

Finalement, nous utilisons un raffinement de NBE de type catégoriel (en employant les faisceaux et les topologies de Grothendieck) pour établir la complétude de cette approche par rapport à BiCCC. Notons que la relation entre BiCCC et les topologies de Grothendieck a été utilisée par Fiore et Simpson (1997) pour donner une caractérisation, sans syntaxe, de la définissabilité des fonctionnels ensemblistes dans le calcul ci-dessus.

Bien qu’un procédé de décision ait été annoncé par Ghani (1994), notre méthode est assez différent et, nous pensons, conceptuellement plus simple; il comprend, également, le cas de produits de types avec un objet initial.

Address: LFCS Edinburgh, Mayfield Rd, Edinburgh EH9 3JZ, United Kingdom

E-mail: mxh@dcs.ed.ac.uk