Paper Info
Title
About systems of equations, X-separability, and left-invertibility in the &lgr;-calculus
Abstract
A system of equations in the λ-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 L = (Γ, X) is said to be solvable in the theory T (T-solvable) iff there exists a suitable simultaneous substitution for the unknowns that makes the equations of L theorems in the theory T. For any finite system and within any semisensible (sms) theory T (e.g., β, βη, H∗) a necessary condition for T-solvability is proved. A class of systems for which this condition also becomes sufficient is shown and the sufficiency is proved constructively. This class properly contains the systems L = (Γ, {x1,…,xn}) that satisfy 0,1 or 0,2 of the following hypotheses: Hp.0. (0) If Q is a proper subterm of a LHS term of an equation and the head of Q is an unknown then the degree of Q is not too large.(1) The initial part of a LHS term never collapses with another LHS term.Hp.1. The equations of S have the shape xM1 … Mn = yx1 … xwM1 … Mn, where x ϵ {x1, …, xu,} and y does not occur in the LHS terms of the equations of L.Hp.2. The equations of L have the shape xM1 … Mn = N, where x ϵ {x1, …, xu,} and N is a βη-normal form whose free variables do not occur in the LHS terms of the equations of L.
Year
DOI
Venue
1991
10.1016/0890-5401(91)90057-9
Inf. Comput.
Keywords
Field
DocType
system of equations,lambda calculus
Discrete mathematics,Pairwise comparison,Finite set,System of linear equations,Existential quantification,Constructive,Free variables and bound variables,Mathematics,Calculus
Journal
Volume
Issue
ISSN
90
1
0890-5401
Citations 
PageRank 
References 
2
0.60
0
Authors
2
Name
Order
Citations
PageRank
Corrado Böhm1487413.44
Enrico Tronci233635.83