# 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 functinos 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.