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.

Back to Homepage: