This thesis studies the Constraint Language for Lambda Structures (CLLS), which is interpreted over lambda terms represented
as tree-like structures. Our main focus is on the processing of
parallelism constraints, a construct of CLLS. A parallelism constraint
states that two pieces of a tree have the same structure.
We present a sound and complete semi-decision procedure for
parallelism constraints, which tests satisfiability and makes
structural isomorphism explicit. This procedure is extended to a
semi-decision procedure for CLLS.
We discuss two applications of CLLS. First, CLLS has been developed as
a formalism for underspecified natural language semantics. In
this context, parallelism constraints are used for modeling parallelism
phenomena. Second, we consider underspecified beta reduction, which is
beta reduction on partial descriptions of lambda terms. For these
application areas, we present extensions both to the language CLLS and to
the semi-decision procedure.