Lambdas

Lambda binding is available as an extension to the theory of arrays.

Syntax and Semantics

Lambda expressions use syntax similar to quantifiers. It is of the form:

(lambda ((x X) (y Y) (z Z)) t)

where x y z are lambda bound variables and t is an expression that can contain the bound variables.

The laws of lambda calculus apply. The simplifier performs $\beta$ reduction.

Other rules $\alpha$ (renaming) and $\eta$ (extensionality) are enforced by the solver.

Inlining definitions using Lambda

The main utility of lambdas in Z3 is for introducing inline definitions as the following memset example illustrates.

Note that the type of (lambda ((x Int)) (if (and (<= lo x) (<= x hi)) y (m x))) is (Array Int Int).

Lambdas as Arrays

Thus, the type of a lambda expression is an array where the domain of the array are the argument types and the range is the sort of the body of the lambda expression.

Thus, in z3 arrays are synonymous with function spaces. You can transition between arrays and functions using as-array to convert a function to an array and using function macros to treat an array as a function. The example also illustrates a subtle use of recursive function declarations. Functions declared using define-fun-rec are expanded on demand and therefore the function symbols are available as arguments to as-array. This contrasts with functions declared using define-fun that are treated as macros that are expanded at parse time. Their function symbols cannot be passed to as-array.

From First-Order to limited Higher-Order

There is limited true higher order reasoning. One basic example that does work thanks to model construction of MBQI instantiation procedure is establishing a second-order definition for equality.

During instantiation, z3 determines to instantiate q with the term (lambda ((z Int)) (= x z)) and therefore it infers the fact (= (= x x) (= x y)). Note that the example illustrates using an array as a function application. We wrote (q x) instead of (select q x) for the array q. It is a feature that is supported as a convenience: the parser performs a best-effort coercions to insert select automatically.

Higher-Order Matching and Term Enumeration

Z3 5.3 and later

Z3 5.3 adds higher-order matching and a quantifier engine that can combine it with term enumeration. This example is non-interactive because the guide's embedded solver uses Z3 5.0; run it with Z3 5.3 or later.

An array-sorted quantified variable can stand for a function or predicate. Ordinary first-order pattern matching cannot always discover the function needed for an instantiation: that function might be a lambda expression that does not occur in the input. Higher-order matching can synthesize such lambdas, and term enumeration supplies additional candidate terms.

The following example quantifies over predicates on an uninterpreted sort U. Its quantified assertion forces arrays a and b to have equal values at every index: if their values differed, a predicate distinguishing them would violate the assertion. Array extensionality then forces a = b, contradicting the different truth values assigned to q a and q b.

(set-option :smt.ho_matching true)
(set-option :smt.ho_qmatcher true)
(set-option :smt.term_enumeration true)
(set-option :smt.ho_matching_bound 1000)
(declare-sort U 0)
(declare-const a (Array U U))
(declare-const b (Array U U))
(declare-fun q ((Array U U)) Bool)
(assert
  (forall ((P (Array U Bool)) (X U))
    (=> (select P (select a X)) (select P (select b X)))))
(assert (q b))
(assert (not (q a)))
(check-sat)

The result is unsat. The three search switches are disabled by default, and the techniques remain incomplete. The matching bound limits expansion work; raising it is not a completeness guarantee. This is still Z3's array/lambda encoding, not a separate function sort or an SMT-LIB 3 frontend. See Quantifiers for the controls and Simplifiers for preprocessing lambda definitions and predicate instantiations.