×

Un résultat de complétude pour les substitutions explicites. (A completeness result for explicit substitutions). (French) Zbl 0717.68053

Summary: We establish a completeness result of \(\lambda\sigma\)-calculus with respect to \(\lambda\)-calculus. Specifically we construct an interpretation of \(\lambda\sigma\)-calculus into \(\lambda\)-calculus, which is such that a source term is typable iff its translation is typable (with the same type). We restrict ourselves to first-order types.

MSC:

68W30 Symbolic computation and algebraic computation
03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite