Describing lambda terms in context unification

Abstract

The constraint language for lambda structures (CLLS) is a description language for lambda terms. CLLS provides parallelism constraints to talk about the tree structure of lambda terms, and lambda binding constraints to specify variable binding. Parallelism constraints alone have the same expressiveness as context unification. In this paper, we show that lambda binding constraints can also be expressed in context unification when permitting tree regular constraints.