Skip to main content

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.