Finite Lambda Model Applet

Finite Lambda Models are a reasoning tool for proving the inequality of untyped lambda terms with respect to beta- or beta-eta equivalence.

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.

Your browser does not run this applet, for some reason. Here is what it would look like:

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.