Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus.

Sylvain Salvati 1
1 SIGNES - Linguistic signs, grammar and meaning: computational logic for natural language
Université Sciences et Technologies - Bordeaux 1, Inria Bordeaux - Sud-Ouest, École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), CNRS - Centre National de la Recherche Scientifique : UMR5800
Abstract : We introduce syntactic descriptions, an extended type sys- tem for the linear lambda-calculus. With this type system checking that a linear lambda-term normalizes to another one reduces to type-checking. As a consequence this type system can be seen as a formal tool to design matching algorithms. In that respect, solving matching equations becomes a combination of type inference and proof search. We present such an algorithm for linear matching equations.In the case of second order equations, this algorithm stresses the similarities between linear matching in the linear lambda-calculus and linear context matching. It uses tabular techniques and is a practical alternative to Huet's algorithm for those equations.
Type de document :
Communication dans un congrès
Frank Pfenning. 17th International Conference on Rewriting Techniques and Applications, RTA 2006, 2006, Seattle, United States. Springer-Verlag, LNCS 4098, pp.151-165, 2006, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00334006
Contributeur : Sylvain Salvati <>
Soumis le : vendredi 24 octobre 2008 - 14:21:02
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13

Identifiants

  • HAL Id : inria-00334006, version 1

Collections

Citation

Sylvain Salvati. Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus.. Frank Pfenning. 17th International Conference on Rewriting Techniques and Applications, RTA 2006, 2006, Seattle, United States. Springer-Verlag, LNCS 4098, pp.151-165, 2006, Lecture Notes in Computer Science. 〈inria-00334006〉

Partager

Métriques

Consultations de la notice

86