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)
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 reduction.
Other rules (renaming) and (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
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
This contrasts functinos declared using
define-fun that are treated as macros that are expanded at parse time. Their function symbols cannot be passed to
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
It is a feature that is supported as a convenience: the parser performs a best-effort coercions to insert