Finite Lambda Models are a reasoning tool for proving the inequality of untyped lambda terms with respect to beta- or beta-eta equivalence. They are described in my paper Order-Incompleteness and Finite Lambda Models, and in my thesis.

This applet allows you to edit a finite lambda model and several lambda terms. It checks that the model you are entering is well-defined, and automatically calculates the term denotations. The applet consists of three parts:

**Poset Editor.**
Here you can create a small poset. Click to create nodes. Drag to
create edges. Click on nodes or edges to highlight them. Drag
highlighted nodes to move them. Double-click or shift-click for
highlighting and moving in one step. Press delete, backspace, or "d"
to delete a highlighted edge or node. The nodes of the poset are
automatically labeled. Press "l" to switch the labels on and off. To
change the labels, use the Binary Operation Editor. Press "p" to print
a representation of the current finite model to standard output; this
works only with appletviewer, not with Netscape.

**Binary Operation Editor.**
Here you can edit the multiplication table for a binary application
operation on your poset. Move around with the arrow keys, return, and
tab keys. Enter upper- or lowercase letters to change an entry. For
the operation to yield a well-defined finite lambda model, it must be
both monotone and strongly extensional. The status line indicates
whether this is the case. If the status line does not display "Okay",
then no term denotations are calculated and a blue background in the
multiplication table indicates a place where monotonicity or strong
extensionality fails.

The operation being edited is really partial. To account for this, an implicit "bottom" element is always added to the poset being edited in the Poset Editor. An empty entry in the multiplication table corresponds to this bottom element. If all entries are non-empty, and the poset you have entered is pointed, then you can ignore this implicit bottom element, as it will never become a term denotation.

**Lambda Term Editor** In each panel, you can edit an untyped
lambda term using standard syntax. The backslash "\" is used for
lambda, and a dot "." must be used to separate abstractors. For
instance, `\x.x`

and `\xyz.x(y\c.c)`

are
well-formed terms. Constant symbols, corresponding to the elements of
the finite model, can be used. Constant symbols consisting of more
than one letter are enclosed in curly brackets such as {bot}.
Variables cannot be enclosed in curly brackets and must always consist
of a single letter. Thus, note that in \x.{x}, {x} is interpreted as a
constant symbol, not as a bound variable.
You can generate or delete panels by using the "More Terms" and "Fewer
Terms" buttons.

If the status displayed beneath the binary operation editor is "Okay", then your model is well-defined, and the denotations of all syntactically correct terms will be automatically calculated and updated. Terms that use unknown constant symbols generate an error message.

**Soundness.**
If the status line shows "Okay" and two term denotations are
incompatible, then it follows that these terms are different with
respect to beta-equivalence. Moreover, if the status line shows that
the model is also order-extensional, it follows that the terms are
different with respect to beta-eta-equivalence.

Copyright 1998 Peter Selinger. This is version 1.3. The source is here.

**Note on portability.**
Unfortunately, Java is not 100% portable, and some features do not
seem to work on all platforms, particularly double-clicking,
shift-clicking and the use of the arrow keys. I have tried to provide
enough alternative keystrokes so that this doesn't become a problem.
I have also tried to stick to Java 1.0, since many browsers do not
(yet) support 1.1.

**Applet parameters.**

`bugfix:`

if present, we work around a scrollbar bug in appletviewer for Solaris JDK 1.1.5`initterms:`

a semicolon-separated list of lambda terms to display initially`finmodinit:`

a semicolon-separated list of instructions for the initialization of the poset and binary operation. The best way to create such a string is by typing "p" in the poset editor; this will export the current finite model to standard output, but this works only in appletviewer. Each instruction is of the form`nodelist [ < nodelist ]...`

or`nodelist * nodelist = node`

. A nodelist is either a wildcard "`_`

" standing for all currently known nodes, or a comma-separated list of nodes. A node is either`label`

or`label(x,y)`

, where`x`

and`y`

are double constants giving the relative coordinates of the node (0=left,1=right,0=bottom,1=top). The instructions are parsed left-to-right. When a node is first mentioned, coordinates must be given. Notice that the blank-statement "`_<_`

" sets all inequalities that are geometrically possible. Non-sensible instructions are ignored or interpreted in a non-predictable way, but no errors are generated.`posetdim:`

the dimensions of the poset editor canvas in the form`width x height`

.

selinger@mathstat.dal.ca / PGP key