Equational programming in λ-calculus

Author

Tronci, Enrico

Author_Institution

Dept. of Math., Carnegie Mellon Univ., Pittsburgh, PA, USA

fYear

1991

fDate

15-18 July 1991

Firstpage

191

Lastpage

202

Abstract

A system of equations in λ-calculus is a pair (Γ, X) where Γ is a set of formulas of Λ (the equations) and X is a finite set of variables of Λ (the unknowns). A system S=(Γ, X) is said to be solvable in the theory T (T-solvable) if there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the formulas of Γ theorems in the theory T. A class of systems for which the β-solvability problem is decidable in polynomial time is defined. This class yields an equational programming language in which constraints on the code generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way

Keywords

computational complexity; decidability; formal logic; logic programming; β-solvability problem; λ-calculus; closed λ-terms; compiler; data structures; decidable; equational programming language; equations; polynomial time; simultaneous substitution; unknowns; Automatic programming; Calculus; Computer languages; Data structures; Equations; Functional programming; Mathematics; Polynomials; Program processors;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on

Conference_Location

Amsterdam

Print_ISBN

0-8186-2230-X

Type

conf

DOI

10.1109/LICS.1991.151644

Filename

151644