The lambda notebook package: linguistic semantics in Python and Jupyter

Author

Kyle Rawlins

Published

August 25, 2024

%%lamb
||a|| = L f_<e,t> : L g_<e,t> : Exists x_e : f(x) >> g(x)
||cat|| = L x_e : Cat_<e,t>(x)
||meowed|| = L x_e : Meowed_<e,t>(x)

$[\![\text{\textbf{a}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \exists{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$
$[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: {Cat}({x})$
$[\![\text{\textbf{meowed}}]\!]^{}_{\left\langle{}e,t\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: {Meowed}({x})$

((a * cat) * meowed).tree()

1 composition path:

$[\![\text{\textbf{a}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}}$

$\lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \exists{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$

$[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}}$

$\lambda{} x_{e} \: . \: {Cat}({x})$

[FA]

$[\![\text{\textbf{[a cat]}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}}$

$\lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \exists{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {g}({x})$

$[\![\text{\textbf{meowed}}]\!]^{}_{\left\langle{}e,t\right\rangle{}}$

$\lambda{} x_{e} \: . \: {Meowed}({x})$

[FA]

$[\![\text{\textbf{[[a cat] meowed]}}]\!]^{}_{t}$

$\exists{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {Meowed}({x})$

1 Package overview

The lambda notebook is a package and framework for doing linguistic semantics (especially compositional semantics) in Python and Jupyter, as well as for working with the standard underlying formal systems used in this field. Some use cases for the lambda notebook include:

doing and verifying calculations involving typed lambda calculus
doing and verifying calculations involving (mostly first-order) logics (including propositional / predicate logic, but also variants and enhanced systems)
implementing a research paper’s analysis in order to understand it better
writing ‘digital fragments’ – working implementations of a compositional analysis or system developed in the course of linguistics research. These could form an appendix or supplementary materials to a paper
implementing a computational semantics model that makes use of core linguistic theory
Using tools like quarto to render linguistic semantics for the web
…

The package consists of several pieces:

A flexible and detailed implementation of metalanguage elements used in linguistics
An implementation of the standard tools for type theory in this field, as well as underlying “natural language ontology”
A framework for building “composition systems” using these metalanguage tools
Tools for rendering objects involved in 1-3 in a way that will be familiar and readable to theoretical linguists, in the context of a Jupyter Notebook

2 Installation and logistics

To install the release version from PyPI, use the pip command line tool: pip install lambda-notebook. On managed jupyter-based systems such as google colab, you can install by entering !pip install lambda-notebook into a notebook cell. The current unreleased version of the package can also be installed from source via the github repository: https://github.com/rawlins/lambda-notebook. On a managed system, the simplest way to do this is to run !pip install git+https://github.com/rawlins/lambda-notebook. Please report bugs on that repository via the issue tracker on github if you encounter any!

Once it is installed, to activate the package, you can either open a notebook with the newly installed kernal named “Lambda Notebook (Python 3)”, or in a regular Python 3 kernel, equivalently run:

import lamb.auto

The above command or kernel installs several “IPython magics” that are a key part of working with a lambda notebook document interactively, and injects some useful functions into an IPython namespace. However, if you’d like to import the package without automatically installing these, import lamb will of course work as expected.

To use the package from the command line, assuming the IPython interpreter is installed, you can also run:

$ python -m lamb.console

This will start a version of the IPython command line interpreter that has the lambda notebook kernel active, and supports lambda notebook magics.

3 Basic usage

This package has quite a lot of moving parts; this section just gives a brief overview.

3.1 Working with the metalanguage

The lambda notebook metalanguage is flexible, python-esque typed language that is parsed into structured python objects. One way of instantiating metalanguage objects is to use the %te line magic. The following example builds and renders a universally quantified logical expression:

%te Forall x_e : P_<e,t>(x)

$\forall{} x_{e} \: . \: {P}({x})$

The following example builds and renders a lambda expression containing a quantified expression. In addition, it assigns the value of this expression to the python variable f:

f = %te L x_e : Forall y_e : Q(x,y)
f

INFO (core): Coerced guessed type for 'Q_t' into <(e,e),t>, to match argument '(x_e, y_e)'

$\lambda{} x_{e} \: . \: \forall{} y_{e} \: . \: {Q}({x}, {y})$

f can now be examined and manipulated in various ways, for example by using indexing to inspect its structure, or looking at its type property.

f[1]

$\forall{} y_{e} \: . \: {Q}({x}_{e}, {y})$

f.type

$\left\langle{}e,t\right\rangle{}$

More info: For more information on the metalanguage and its capabilities, see the various documentation notebooks in the source repository.

3.2 Working with composition systems

You can use metalanguage objects to define lexical entries that can the be composed with a “composition system” – a collection of composition operations. The default composition system is a standard one with Function Application and several other rules familiar from e.g. Heim and Kratzer 1998.

To replicate the starting example in this document, we can first define lexical entries for the three words using metalanguage code in the %%lamb cell magic:

%%lamb
||every|| = L f_<e,t> : L g_<e,t> : Forall x_e : f(x) >> g(x)
||cat|| = L x_e : Cat_<e,t>(x)
||meowed|| = L x_e : Meowed_<e,t>(x)

$[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$
$[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: {Cat}({x})$
$[\![\text{\textbf{meowed}}]\!]^{}_{\left\langle{}e,t\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: {Meowed}({x})$

The rendered outputs will look relatively familiar from an introductory semantics class. Lexical entries defined this way are also exported to the outer namespace in a jupyter context, so we can refer to the entries via their names in python as well. Now that these entries are defined, the python * operator is overloaded to do composition according to the current composition system. For example, to compose “every” and “cat” above, we can simply write:

every * cat

1 composition path. Result:
[0]: $[\![\text{\textbf{[every cat]}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}} \:=\: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {g}({x})$

There’s quite a lot of manipulation and introspection that can be done with composition objects, but for example, the following shows a step by step breakdown with the rules indicated:

(every * cat).trace()

Full composition trace. 1 path:
    Step 1: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$
    Step 2: $[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: {Cat}({x})$
    Step 3: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}}$ * $[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}}$ leads to: $[\![\text{\textbf{[every cat]}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}} \:=\: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {g}({x})$ [by FA]

The following (which adds the main verb as well) shows a more complex sequence with a tree-like visualization:

((every * cat) * meowed).tree()

1 composition path:

$[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}}$

$\lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$

$[\![\text{\textbf{cat}}]\!]^{}_{\left\langle{}e,t\right\rangle{}}$

$\lambda{} x_{e} \: . \: {Cat}({x})$

[FA]

$[\![\text{\textbf{[every cat]}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}}$

$\lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {g}({x})$

$[\![\text{\textbf{meowed}}]\!]^{}_{\left\langle{}e,t\right\rangle{}}$

$\lambda{} x_{e} \: . \: {Meowed}({x})$

[FA]

$[\![\text{\textbf{[[every cat] meowed]}}]\!]^{}_{t}$

$\forall{} x_{e} \: . \: {Cat}({x}) \rightarrow{} {Meowed}({x})$

Of course, Function Application (and other composition rules) will ensure that types are verified, and composition won’t succeed if the types are mismatched. For example, “every” wouldn’t be able to compose directly with a two-place (type $\langle e, \langle e,t \rangle \rangle$) predicate:

%%lamb
||sister|| = L x_e  : L y_e : SisterOf(y,x)

INFO (core): Coerced guessed type for 'SisterOf_t' into <(e,e),t>, to match argument '(y_e, x_e)'

$[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$

every * sister

Composition of “[every sister]” failed:
    TypeMismatch: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ and $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ conflict (Function Application needs a matching function and argument)
    TypeMismatch: $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ and $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ conflict (Function Application needs a matching function and argument)
    TypeMismatch: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ and $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ conflict (Predicate Modification needs property types)
    Composition failure on: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ * $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ (Predicate Abstraction requires a valid binder)
    Composition failure on: $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ * $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ (Predicate Abstraction requires a valid binder)
    TypeMismatch: $[\![\text{\textbf{every}}]\!]^{}_{\left\langle{}\left\langle{}e,t\right\rangle{},\left\langle{}\left\langle{}e,t\right\rangle{},t\right\rangle{}\right\rangle{}} \:=\: \lambda{} f_{\left\langle{}e,t\right\rangle{}} \: . \: \lambda{} g_{\left\langle{}e,t\right\rangle{}} \: . \: \forall{} x_{e} \: . \: {f}({x}) \rightarrow{} {g}({x})$ and $[\![\text{\textbf{sister}}]\!]^{}_{\left\langle{}e,\left\langle{}e,t\right\rangle{}\right\rangle{}} \:=\: \lambda{} x_{e} \: . \: \lambda{} y_{e} \: . \: {SisterOf}({y}, {x})$ conflict (Vacuous composition needs at least one fully vacuous element)

You can see from the above that the default composition system has a number of other rules that are tried in addition to standard FA, but of course none of them work in this case.

More info: For more on composition systems and composition, see the interactive documentation notebook as well as many example fragments that illustrate how to do things like modify a composition system.

4 Further resources

The easiest way to get started is to look at examples. As linked above, the package provides many example and documentation notebooks. Note: these are saved in the repository unexecuted (with no output), and meant to be used interactively.

In 2022 I taught a class at the North American Summer School on Logic, Language and Information on the lambda notebook (as it was at the time, of course). The slides and demos provided there may be useful to semanticists and logicians who have minimal computational background.