Decidability of the restriction equational theory in the partial lambda calculus

Abstract:

In his thesis about partially and λ-calculus Eugenio Moggi raised the following conjecture: the equational theory T⌈ (see definition below) corresponding to the restriction in the partial λ-calculus is decidable. Testing the truth of this conjecture is very important because one of the results in Moggi's thesis is the confluence of the partial λ-calculus modulo the theory T⌈. In this paper we justify Moggi's conjecture. © 1989.

Año de publicación:

1989

Keywords:

Fuente:

scopus