Syntactic theories and the algebra of record terms - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1993

Syntactic theories and the algebra of record terms

Didier Rémy
  • Fonction : Auteur
  • PersonId : 915856

Résumé

Recently, many type systems for records have been proposed. For most of them, the types cannot be describes as the terms of an algebra. In this case, type checking or type inference in the case of first order type systems, cannot be derived from existing algorithms. We define record terms as the terms of an equational algebra. We prove decidability of the unification problem for records terms by showing that its equational theory is syntactic. We derive a complete algorithm and prove its determination. We define a notion of canonical terms and approximations of record terms by canonical terms, and show that approximations commute with unification. We also study generic record terms, which extend record terms to model a form os sharing between terms. We prove that the equational theory of generic record terms and that the corresponding unification algorithm always terminates.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-1869.pdf (582.81 Ko) Télécharger le fichier

Dates et versions

inria-00074804 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00074804 , version 1

Citer

Didier Rémy. Syntactic theories and the algebra of record terms. [Research Report] RR-1869, INRIA. 1993. ⟨inria-00074804⟩
94 Consultations
196 Téléchargements

Partager

Gmail Facebook X LinkedIn More