The Penn Lambda Calculator
For students and teachers of natural language semantics
Supported by a University of Pennsylvania SAS technology grant.
The Penn Lambda Calculator is an interactive, graphical, pedagogical computer program that helps students of natural language formal semantics practice the typed lambda calculus. Click on the pictures to the right to see screenshots (1 2 3). Lambda, as we call it for short, was started in June 2006. It has been used, among other places, in Prof. Maribel Romero's course "Introduction to Semantics" (LSA.328) at the 2007 LSA Institute in Stanford.
The goal of the Penn Lambda Calculator project is to provide teachers and students with a software that assists them in mastering the centerpiece of introductory courses to formal semantics: the lambda calculus. The most important feature of this software is its sophisticated routines that detect common errors and return "smart" feedback to the student user. It also has a module for performing derivations of natural language phrases up a syntactic tree in the style of Heim & Kratzer (1998).
The program is described thoroughly in our paper in the proceedings of GEAF 2007:
Champollion, L., J. Tauberer and M. Romero (2007). "The Penn Lambda Calculator: Pedagogical Software for Natural Language Semantics", in T. Holloway King and E. M. Bender (eds.), Proceedings of the Grammar Engineering across Frameworks (GEAF) 2007 Workshop, July 13-15 2007. CSLI On-line Publications [PDF]
But note that the program undergoes ongoing development and several new features have been added since the publication of the GEAF paper.
Several features are currently under development and are not yet publicly available, including:
You can download the current version, which is version 1.0.12 (March 29, 2008; Change Log):
Windows EXE version (no installation necessary; just download and double-click to start)
Java JAR version for all other platforms (Mac OS X, Linux).
On a Mac, just download and double-click to start.
On Linux, start with java -jar LambdaCalculator.jar. (But make sure you run it with Sun's Java, not GNU libgcj, which you can check with java -version.)
About installing Java:
Windows and Linux users will need to make sure they have the Java JRE 1.4 or newer installed. The Windows version of the calculator will check on startup if Java is installed, and if necessary, will take the user to a website where Java can be downloaded.
On Mac OS, Java is already installed in most cases (e.g. Mac OS 10.4 Tiger and upwards come with Java 1.4 or higher installed by default). Otherwise, it can be installed via the Software Update option in the Apple menu. If you are not sure if your Mac has the right version of Java, just try and run the program. If nothing happens or if you get an error message, you'll need to update Java.
The teacher edition, in which tree-derivation exercises are shown in a presentation mode that automatically computes denotations of nonterminals, is available upon request to bona fide instructors. Send an email from your academic email address to:
Regardless of which edition you use, we're interested in hearing from you. We read all user feedback attentively. If you're an instructor, a student, or just a Web passerby, send us a line and tell us about how you use (or would like to use) the program and how we can improve it.
Source code will be posted shortly.
We have three example exercise files:
example1.txt: Examples of 'semantic types' and 'lambda conversion' exercises.
example2.txt: Examples of bottom-up tree derivation exercises.
example3.txt: Examples of using bottom-up tree derivations with generalized quantifiers (including set notation).
You can download these and then open them in the Penn Lambda Calculator to try them out. To download the files, right-click the link (on a PC) or control-click (on a Mac?) and choose "Save Link As..." to save the file to your computer. Remember where you saved the file. Then (download and) run the Penn Lambda Calculator. Choose the Interactive Exercise Solver, and in the File menu, choose Open, and open the exercise file you downloaded.
If you are an instructor, email us, and we will be happy to send you more exercise files. And if you write exercise files yourself, please consider sending them to us so we can share them with other instructors.
For students and instructors: When typing predicate logic expressions in the program, some special keyboard combinations are used to enter logical symbols. See the guide to entering special symbols for instructions. Some help is also provided within the program.
For instructors: If you would like to write an exercise file, you may read the documentation for the exercise file format or consult the complete and documented sample exercise file for instructors.
The Penn Lambda Calculator lets lambda abstraction take precedence over function application. This is the opposite convention as the one used in Heim and Kratzer (1998). Thanks to Irene Heim for pointing this out.
For example, our system parses "λyλx.[R(x,y)](a)(b)" as "[ [ λyλx.R(x,y) ] (a) ] (b)" rather than as "[ λy [ [λx.R(x,y)] (a) ] ] (b)". Specifically, the latter case is ruled out because it would result in the lambda abstraction headed by λy having as its body an instance of function application, i.e. "[[λx.R(x,y)] (a) ]". The same precedence rule holds of variable binders other than lambdas, specifically quantifiers and iota operators.
There is, however, an exception to this rule: Although the relations between atomic predicates and their arguments are semantically interpreted as function application, they nevertheless take precedence over lambda abstraction, and in fact over all other operators. This is so that "λx.P(x)" is parsed as "λx.[P(x)]" and not as "[λx.P](x)". This also applies to Schönfinkelized predicates; e.g. the expression "λx.R(x)(a)" is parsed as "λx.[R(x)(a)]".