Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
Chapter 4: Higher-Order Equational Reasoning.
Chapter 5: Decidability of Higher-Order Unification.
Chapter 1: Introduction. The topic of the book is equational reasoning (in the form of rewriting) in higher-order logic. Techniques for such reasoning can be used to integrate functional and logic programming, as, for example, in lambda-Prolog. Prehofer's approach is to use higher-order narrowing as an inference rule to solve equations with (existentially quantified) variables.
It is well-known that higher-order unification is undecidable. However, there are decidable classes of problems which may be sufficient for functional-logic programming. These decidable classes (for second-order problems) are discussed later in the book. Given restrictions on the rewrite rules (such as left-linearity), there are narrowing techniques which use decidable unification and a call-by-need strategy. Applications of higher-order narrowing are included near the end of the book.
Chapter 2: Preview. First-order term rewriting and narrowing are introduced. Lazy narrowing incorporates unification into the narrowing process and works in an "outermost" fashion. Logic Programming can be extended to use narrowing by viewing predicates as functions which rewrite to "true." Term rewriting can be extended to the higher-order case (simply typed lambda calculus with alpha and beta conversions). To extend narrowing to the higher-order case, we face the problem of higher-order unification.
In higher order unification we may have an infinite set of incompatible solutions, such as the solution set {F -> lambda x . f^n x : n} for the problem "lambda x [F(f(x))] =? lambda x [f(F(x))]" [this is modified from his example].
"The first complete set of rules for higher-order unification was presented by Jensen and Pietrzykowski [1973, 1976]." Huet [1973] and Lucchesi [1972] showed third-order unification to be undecidable. Goldfarb [1981] showed second-order unification is undecidable, and Farmer [1991] showed that only one arity two symbol is needed to show undecidability in the second order case. Monadic second-order unification is decidable since it can be reduced to unification modulo associativity (monoid unification) and this problem was shown decidable by Makanin [1977]. Monadic third-order unification is undecidable [Narendran, 1989].
Third-order matching was shown decidable by Dowek [1992] and fourth-order matching was shown decidable by Padovani [1995]. The general higher-order case is an open question. Dale Miller identified the class of patterns (lambda terms where the frees have only distinct bounds as arguments) for which unification is decidable and unitary (there is a single MGU). In full higher-order unification, we are not guaranteed the existence of maximally general unifiers ("nullary unification"--there may be an infinite set of unifiers, each more general than the next). This was noted by Gould [1966]. Huet [1975] invented pre-unification [though he did not use this term] which delays flex-flex pairs and enumerates a complete set of [preunifiers] without any redundancy. Preunification is still infinitary.
Prehofer identifies certain classes of decidable unification problems. For example, unifying linear higher-order patterns with variable-distinct arbitrary second-order terms is decidable and finitary. (Note this is a result about unification, not preunification.) Another decidable case is unifying certain second-order terms (which have the form of induction schemes) with first-order terms.
Higher order narrowing is considered with terminating rewrite systems R. This involves starting with a problem "LHS ->? RHS" where the RHS is R-normal. The problem is to find substitutions for the free variables so that the instantiated LHS rewrites to the RHS via R. At some point in the narrowing process, we may encounter goals such as "X ->? RHS." In this case (at least in Prehofer's setting), we can eliminate X by replacing it with RHS throughout the problem. On the other hand, goals such as "LHS ->? X" should not be eliminated--this corresponds to a "call by need" strategy.
The restriction to linear terms is motivated by the fact that "functional-logic programming can be viewed as a special case of narrowing with left-linear rewrite rules." For such rewrite systems, goals called "Simple Systems" (in which no variable occurs twice on the RHS's of the system of goals and "there are no cyclic dependencies between variable occurrences in goals"). For such systems, we cannot have occurs-check [fixed point] problems. Solved forms of Simple Systems are of the form "t1 ->? X1, . . ., tn ->? Xn."
A further extension of narrowing yields conditional narrowing. Here, we restrict ourselves to the case of normal conditional rules "l -> r <== l1 -> r1, . . ., ln -> rn" where each ri is a ground R-normal term. [Consider, for example, a case of the form "l -> r <== p1 -> true, . . ., pn -> true."]
Chapter 3: Preliminaries. The basic terminology of reductions is introduced (reflexive transitive closure, equivalence relations, partial orderings, total orderings, terminating reductions, normal forms, joinability, local confluence and confluence). Next the language of simply typed lambda calculus is introduced, along with alpha-, beta-, and eta-conversion. Beta-normal form, eta-normal form, and long beta-eta form are defined. Long beta-eta form is generally used. A variable is isolated if it only occurs once. Linear terms are those in which no free variable occurs repeatedly. A term "lambda x-bar . tau t-bar" is flexible if tau is a free variable and rigid otherwise. We work modulo alpha-conversion, which can be made precise using de Bruijn indices [1972]. We also intuitively consider bound variables and free variables to be distinct--note that using this convention we may have "loose" bound variables (which are to be treated as if they are "bound in context"). The notion of "positions" of subterms of lambda terms can be made precise using sequences of natural numbers, where the empty sequence is the top position, a 1 means "pop one lambda abstractor," and an i means "take the i'th argument of the application."
The order of a type phi is defined inductively: Ord(beta) = 1 for base types beta; Ord(alpha_1 -> . . . -> alpha_n -> beta) = 1 + k where beta is a base type and k is max(Ord(alpha_i)). A symbol is order n if its type is order n. A term of order n uses function constants of order <= n+1 and variables of order <= n. A weakly second-order term is second-order except that frees may have arbitrary bound variables (up to eta) as arguments. (Example: F(lam z.x(z),y) is weakly second order, not second order--think F(x,y) where x is not of base type.)
Substitutions theta are defined as finite mappings from variables to terms [of the same type]. Dom(theta) is the set of free variables which are not mapped to themselves, and Rng(theta) is the set of variables free in the images of each X in Dom(theta). Substitutions may be equal on a set of variables, restricted to a set of variables, and composed. A substitution may be more general than another (over a set of variables). A substitution may be idempotent (in particular if the Dom and Rng are disjoint). Properties of terms (such as being in long beta-eta-form) can be naturally extended from terms to substitutions by considering images.
E-unification is the problem of finding substitutions theta so that theta(s) =E theta(t) (where E is an equivalence relation on terms). A minimal complete set of unifiers (MCSU) of an E-unification problem s =? t is a set of E-incomparable E-unifiers S so that every E-unifier is more E-specific than some E-unifier in S. We can classify such problems based on the nature of MCSU's. A problem is:
"unitary if a MCSU is either empty or a singleton
finitary if a finite MCSU exists
infinitary if a possibly infinite MCSU exists
nullary if no MCSU may exist"
"This classification extends to an equational theory E, if for all E-unification problems the property holds."
A relaxed higher-order pattern is a simply typed lambda-term s so that all free variables in s have only (terms which eta-reduce to) bound variables as arguments. Such a term is a higher-order pattern [Miller 1991a] if these bound variables are distinct. Unification of patterns is decidable and unitary (and a most general unifier can be computed in linear time [Qian 1993].
Chapter 4: Higher-Order Equational Reasoning. A sound and complete transformation system PT for higher-order pre-unification (adapted from Snyder and Gallier [1989]) is introduced. The system consists of the deletion, decomposition, elimination, imitation and projection rules. The system generates pre-unifiers (note that the notions of MCSU and unification classes can be extended to preunification). Also, when concerned with second-order unification problems, the projection rule can only generate projection terms of the form "lambda x1 . . . lambda xn xi" since xi must have base type. Imitation and projection compute substitutions which map variables to higher-order patterns.
Pattern unification is decidable and unitary. A transformation system PU for pattern unification is given, which consists of the rules deletion, decomposition, elimination, imitation/projection (which can be treated in one case since there can be no choice), flex-flex same (in which the heads are the same variable and we only keep those arguments which are the same bound variable on both sides), and flex-flex diff (in which the heads are different variables and we keep the intersection of those bound variables which appear as arguments). Note that any lambda-term can be "flattened" into a pattern part and "constraints" so that if p and q can be unified then the corresponding pattern parts p' and q' can be unified (giving a decidable necessary condition for general unification).
A higher-order rewrite rule is a l -> r so that l is not eta-equivalent to a free variable and l and r are long beta-eta-forms of the same base type. A General Higher-Order Rewrite System (GHRS) is a set of such rewrite rules. From this we can define a rewrite step in the usual way. However, we must be careful because a subterm may contain free variables which are bound in context ("loose bounds"). This if formally handled by "x_k-lifters"--substitutions which replace free variables F to rhoF x_1 . . . x_k where rhoF is a new variable of appropriate type.
An HRS is a GHRS with patterns on each LHS. A pattern rule has patterns on both sides, and a pattern HRS is an HRS of such rules. Left-linear rules have linear LHS's.
We can also partition constants into constructors and defined symbols. We can also distinguish between innermost and outermost rewrite steps. Innermost rewriting corresponds to eager evaluation, while outermost rewriting corresponds to call-by-name evaluation. Each GHRS generates an equivalence on terms.
Two (HRS) rules have an overlap if a nonvariable subterm of one lefthand side unifies with the other lefthand side. An HRS is orthogonal if it is left-linear and has no overlaps. Orthogonal HRS are confluent. Each overlap gives a critical pair. An HRS is locally confluent iff all critical pairs are joinable. A locally confluent, terminating HRS is confluent [we do need termination]. Termination of an HRS is generally undecidable, but can be determined in special cases using the method of termination orderings.
Chapter 5: Decidability of Higher-Order Unification. We first consider "elimination problems," i.e., problems of the form "lambda x_1 . . . lambda x_n [P y_1 . . . y_m] =? lambda x_1 . . . lambda x_n . t" where P is not free in t (and the y_j's are distinct x_i's, so the LHS is a pattern). Note that such problems include the flex-flex case (so solving such problems will allow us to perform unification instead of preunification in such cases). The problem is that P can only depend on the x_i's in the list of y_j's, so we need to substitute for the free variables in t in such a way that eliminates dependence on variables in W = {x_i} - {y_j}. There may be multiple ways of doing this. Example 5.1.1. "lambda x, y [F x] =? lambda x,y . F'(F''(x),F''(y))." Here we need to eliminate the y, which we may do by either taking F' to be "lambda u,v F'_1 u" or taking F'' to be "lambda u F''_1." The number of different unifiers is, however, quadratic in the size of the term t (it is bounded by mn where m is the maximum number of nested frees and n is the number of occurrences of variables to be eliminated). A transformation system EL is presented which computes the most general such substitutions--so this problem is finitary. (Of course, the unifier, once we have such a substitution theta, is theta union {F -> lambda y-bar [beta-normalize(theta(t))]}.) The correctness and completeness of EL is proven.
The systems PU and EL can be combined to show the following important result: If theta is a MGU of two patterns s and t, then either theta(s) has fewer free variables than s and t (combined) or theta is not size-increasing. This result holds because we can use deletion, decomposition, and the flex-flex cases from PU (these give substitutions which are not size increasing) and use EL instead of elimination and imitation/projection. The system EL obviously decreases the number of variables since a substitution is applied to the "P" in the pattern head position (and the other EL rules generate substitutions which do not increase the number of variables).
We can extend this problem to include the case where some y_j's are repetitions (so the LHS is a relaxed pattern). In this case we may get an exponential number of solutions, as is suggested by the example "lambda x [F x x] =? lambda x [c x]" but it is still finitary. The system EL generates substitutions which can be used to find all appropriate permutations corresponding to the different unifiers.
Unifying a linear pattern with a variable-disjoint weakly second-order term is decidable and finitary. The system PT is shown to terminate in such a case (using a well-ordering to prove termination) with flex-flex pairs of a form that can be solved using EL (although the LHS of these flex-flex pairs may be relaxed patterns, not just patterns).
The fact that the possibility of second-order unification is undecidable implies that the possibility of second-order unification with the LHS linear is also undecidable by considering the problem "lambda x [F [f x G]] =? lambda x [g [f x t_1] [f x t_2]]" where t_1 and t_2 are arbitrary second-order terms. So, we cannot get rid of the restriction that the LHS be a pattern. (Similarly, the easier example "lambda x [x F F] =? lambda x [x t_1 t_2]" shows we cannot get rid of the restriction that the LHS be linear.)
However, we can relax the restriction that the LHS must be a pattern by assuming the arguments to free variables on the LHS be either bound variables or ground second-order terms of base type (no nested free variables). In this case we use the fact that second-order matching is decidable (and has ground substitutions as solutions [note general higher-order matching may not return ground solutions!]) to show the pre-unification problem is decidable and finitary, using system PT. We can use such problems to decide a second-order unification problem "s =? t" where s is as above, except we allow arguments to s to be (not ground) second order terms of base type as long as no outside bound variables occur in these arguments. Such a problem can be reduced to the previous problem by replacing such terms with new bound variables which we abstract on both sides. The new problem is unifiable iff the previous problem was (but this does not give us a complete set of unifiers, and so does not imply the problem is finitary). We do, however, have that such problems are decidable. As a special case, we have that the unification problem "s =? t" where s and t are second-order and s contains no bound variables is decidable.
A linear second-order system is a system of the form "lambda x-bar X_n(t_n-bar) =? lambda x-bar t'_n-bar" where all X_n are distinct and do not occur elsewhere and all "lambda x-bar t_n" and "lambda x-bar t'_n" are patterns. This unification problem is decidable, using System PT without elimination [note that elimination is not needed for completeness of PT because we can use projection and imitation to find partial bindings of free variables until we get to the flex-flex case]. This case can be used to solve the more general case where a system is given by "theta(s) =? theta(t)" where s and t are patterns and theta maps variables X to "lambda x-bar X'(t'-bar)" where each t' is a pattern. (example: "f(X(a),X(a)) =? p" where p is a pattern). We solve such a system by first performing pattern unification on "s =? t" and then applying the resulting pattern unification to the system given by theta to yield a linear second-order system.
The next results apply to the problem of unifying first-order terms with second-order induction schemes. A quasi first-order term is of the form "lambda x-bar t" where t is first-order. A "pattern with ground arguments" is a pattern except "arguments to free variables are ground terms which contain at least one outside bound variables but no local binders." (Example: "lambda x . P(x+1,x)") The unification problems "lambda x-bar P(t-bar) =? lambda x-bar t" where the RHS is quasi-first order and the LHS is a pattern with ground arguments is decidable. This result can be used to show that we can decide the following unification problem: Let "lambda x-bar p" be a pattern where no abstractions occur in p, "lambda x-bar P(t_m_n-bar)" be second-order patterns with ground arguments, "lambda x-bar P_n(y-bar)" be patterns, and "lambda x-bar t" quasi first-order. The unification problem "lambda x-bar p =? lambda x-bar t" along with each "lambda x-bar P(t_m_n-bar) =? P_n(y-bar)" where P is not free in "lambda x-bar p" or "lambda x-bar t" is decidable.
Note that while many systems achieve decidability by restricting to patterns, the main restriction Prehofer uses is linearity. This restriction is motivated by higher-order narrowing. The author notes a few open problems.
Give an example of a higher-order unification problem with infinitely many incomparable solutions. Solution
Discuss the history of higher-order unification. (Who gave the first complete set of rules? Who showed undecidability of which classes? Who showed certain classes decidable? Answers
Do these terms mean anything to you? matching, patterns, unitary unification, nullary unification, pre-unification Answers
Give two examples of decidable classes of unification problems identified by Prehofer. Answer
How does the call-by-need narrowing strategy manifest itself with respect to variable eliminations? Answer
Relate functional-logic programming, narrowing with left-linear rewrite rules, and Simple Systems. Idea
Describe conditional narrowing. Answer
Define the order of a type and the order of a term. What is a weakly second-order time? Answer
Define the notion of a minimal, complete set of unifiers (MCSU) for an E-unification problem. Partition E-unification problems into classes based on the existence of MCSU's. Solution
What is a relaxed higher order pattern? What is a higher-order pattern? Classify the unification problem for higher-order patterns. Answers
Describe a sound and complete system for higher-order pre-unification. What are imitation and projection bindings? How do projection bindings specialize in the second order case? What can you say about the image of a variable under an imitation or projection binding? Answers
Give a sound and complete transformation system for pattern unification. Define how to flatten a lambda term so that a unification problem separates into a pattern part and constraints. Give a decidable necessary condition for two terms to be unifiable. Idea
What is a GHRS? Give a formal way to handle "loose" bound variables when applying a rewrite rule to a subterm. Answer
What is an HRS? What are left-linear rules? Answer
Relate rewriting strategies to evaluation strategies. Idea
Define the following notions: overlaps between HRS rules, orthogonal HRS, critical pairs, terminating HRS, convergent HRS. State the related results. Ideas
What is an elimination problem? Describe how to solve such problems and give a bound on the number of solutions. Ideas
What important fact holds given a MGU theta of two patterns s and t? Answer
What changes if we generalize the elimination problem to relaxed patterns? Answer
What can one say about the unification problem between a linear pattern and variable-disjoint weakly second-order term? Answer
Can we decide the unification problem between a linear term and a variable-disjoint second-order term? What about a pattern and a variable-disjoint second-order term? Answers
How can we relax the restriction to patterns (retaining linearity) and still have decidable unification with weakly second-order terms? Answer
Give an example to show that an order 3 matching problem may give a nonground solution. Solution
Describe how to relax the linearity condition by considering linear second-order systems. Answer
Describe a decidable class of unification problems which include certain induction schemes. Solution