This notebook introduces the typed lambda calculus in the context of the Lambda Notebook. It presupposes some knowledge of how similar formalisms are used in compositional semantics. It also isn't intended to generally introduce the lambda notebook's metalanguage.
Note: Run all on this notebook will be blocked by a purposefully generated exception in the middle.
In formal semantics, compositionality is typically modeled by the interaction of (potentially higher order) functions, and this interaction is guided by syntactic structure. Functions are typically characterized using a typed lambda calculus. An untyped lambda calculus uses representations like "$\lambda x \: \alpha $" to characterize a function that given some $x$, returns $\alpha$. A typed lambda calculus uses a system of types to place constraints on both $x$ and $\alpha$, effectively describing the domain and range of the function explicitly. (Often, types are actually defined in terms of sets, but here I will not do that, as the lambda notebook takes them as primitives.)
The two core types in (extensional) formal semantics are $e$ (for entities), and $t$, for truth-values. A functional type is always a pair of types, with the left member specifying the domain, and the right member specifying the range. An inductive definition of (simple) types therefore often takes this form:
Rule 2 is recursive. So, the type $\langle e, t \rangle$ characterizes functions whose domain is the set of entities, and whose range is the set of truth-values. $\langle \langle e, t \rangle, t \rangle$ is the type of a function whose input is a (higher order) function of type $\langle e, t \rangle$, and whose output is type $t$ (this is of course the type of a generalized quantifier). In the Lambda Notebook, types are written in a similar way, and $e$ and $t$ are built in. The following shows how to construct these three types using the built-in tp
(for type parser) function, which parses strings into Type objects.
from IPython.display import display
display(tp("e"),
tp("<e,t>"),
tp("<<e,t>,t>"))
tp("<<e,t>,t>").left
All expressions in the Lambda Notebook metalanguage are typed, including variables and constants, and this is written using a "_
" followed by the type. The following simply defines a variable over functions $f$ that has the type of a generalized quantifier.
%%lamb
f = f_<<e,t>,t>
f.type
See the neo-Davidsonian fragment and the intensional semantics fragments for examples of adding further types.
There are various notational systems/conventions for a typed lambda calculus, but one common notation (or notational shortcut) often seen in formal semantics is to write expressions such as:
In Heim and Kratzer, for example, this is really an abbreviation for something like the following, which is basically a two-place $\lambda$ expression allowing for rich constraints on $x$:
Currently the lambda notebook uses only the abbreviated form, i.e. allows only type-based constraints, not the two-place $\lambda$ expression. Therefore, a lambda expression in the notebook consists of a variable, a type constraint, and a body. These expressions both describe a function that, given some $x$ of type $e$, returns true just in case $x$ is a cat. Notice that, implicitly, the thing to the right of the period is a truth-value, and the predicate $Cat$ can be thought of as having a type as well (though this last part isn't typical; it is often thought of as being a first-order predicate logic constant).
In the lambda notebook, this function can be described in the meta-language using the form "lambda var_type : body
", where the variable name (lowercase) is separated from the type by an underscore. Here's an example:
lambda x_e : Cat(x)
This example is illustrated below in practice. The second line of the next cell defines a variable cat
that is a function of type $\langle e, t \rangle $. This variable is exported into the python environment, and is a subclass of lamb.meta.TypedExpression
(In this case, lamb.meta.LFun
, the class for lambda expressions.)
%%lamb
cat = lambda x_e : Cat(x)
ltx_print(cat, cat.type, "This object's class is: " + str(cat.__class__))
Notice the info message warning us effectively that we didn't specify a type for the constant Cat
. There are some very simple built-in heuristics for what type you might mean, and it first guesses $t$ for a constant (and $e$ for a variable); it realizes this is wrong and upgrades the type for the constant to be a property type. We could also explicitly specify all the types for all terms:
%%lamb
cat = lambda x_e : Cat_<e,t>(x_e)
If you do something wrong, a TypeMismatch
(module: types
) exception will be raised. Note that type checking happens on construction of any TypedExpression
, and is not deferred until application.
%lamb p_t = p_t
%lamb y_e = y_e
cat(y) # this one works, because the types match
cat(y).reduce_all() # a handy function
Here's an example of a type mismatch that you can uncomment if you want; a preformatted example of what happens when this sort of exception is thrown in python is shown below the cell. An exception produces a 'stack trace' showing exactly where execution was when the exception happened, which is often more verbose than you need: for TypeMismatch
the crucial problem is usable visible from the end of the stack trace.
# cat(p)
---------------------------------------------------------------------------
TypeMismatch Traceback (most recent call last)
<ipython-input-10-44e69702d8b9> in <module>()
----> 1 cat(p)
/Users/advil/repos/lambda-notebook/lamb/meta.py in __call__(self, *args)
1160
1161 #print("globals: ", globals())
-> 1162 return TypedExpr.factory(self, *args)
1163
1164
/Users/advil/repos/lambda-notebook/lamb/meta.py in factory(cls, assignment, *args)
821 else:
822 logger.warning("Unable to coerce guessed type %s for '%s' to match argument '%s' (type %s)" % (operator.type, repr(operator), repr(arg), arg.type))
--> 823 result = ApplicationExpr(operator, arg, assignment=assignment)
824 if result.let:
825 result = derived(result.compact_type_vars(), result, "Let substitution")
/Users/advil/repos/lambda-notebook/lamb/meta.py in __init__(self, fun, arg, defer, assignment, type_check)
1271 tc_result = self.fa_type_inference(fun, arg, assignment)
1272 if tc_result is None:
-> 1273 raise TypeMismatch(fun, arg, "Function argument combination (unification failed)")
1274 fun, arg, out_type, history = tc_result
1275 op = "Apply"
TypeMismatch: Type mismatch: '(λ x_e: Cat_<e,t>(x_e))'/<e,t> and 'p_t'/t conflict (mode: Function argument combination (unification failed))
It is often convenient to wrap something that might produce a TypeMismatch directly in a try: ... except: ...
block. Here is one way of doing this:
result = None
try:
result = cat(p)
except types.TypeMismatch as e:
result = e
result
Lambda expressions can be treated just as any expression in the lambda notebook metalanguage, with parenthesis used for grouping (see other documentation for details). For example, we can write very complicated expressions made up of functions:
reload_lamb()
%%lamb
id = ((lambda f_<<e,e>,<e,e>> : lambda g_<e,e> : lambda x_e : (f(g))(x))(lambda h_<e,e> : h))(lambda i_e : i)
The full semantics of lambda expressions (i.e. function argument combination and type checking) are supported. In some cases (mainly semantic composition) reduction is done automatically but for variable definitions like this you have control. The easiest way to do the reduction is typically the reduce_all
function:
id.reduce_all()
If you want to see how this happened, you can peek at the derivation with varying levels of detail:
id.reduce_all().derivation
id.reduce_all().derivation.trace()
Variable renaming of bound variables (alpha conversion) will occur as needed.
%%lamb
collision = lambda x_e : (lambda f_<e,t> : lambda x_e : f(x))(lambda y_e : y <=> x) # use '<=>' for equality
$x$ is of course bound to the higher lambda term in the argument, and we wouldn't want it to become bound to the lower variable on function application (substitution for $f$ in the scope of the lwoer binder), so one of them has to be renamed:
collision.reduce_all()
That's pretty much what there is to the lambda calculus in this context. To summarize:
lambda var_type : body
".%%lamb
environments for defining functions in the metalanguage.Finally, if you want to inspect an existing object to see how you would write it in the meta-language, repr
is guaranteed to produce parsable output with the same result. (If it doesn't, this is a bug, please report it!) The form may be slightly normalized relative to how it was constructed.
repr(collision)
te(repr(collision))
repr(te(repr(collision))) == repr(collision) # normalization should be idempotent, too