Home

Lambda: The Semantics Tool

Lambda is an interactive, graphical, pedagogical computer program that helps students of formal semantics practice the typed lambda calculus.

We discussed how the LC is used in linguistics in the past (check the archives). This tool may be useful even for those not interested in this angle, even though that's the intended use of the software.

By Ehud Lamm at 2007-07-22 17:56 | Lambda Calculus | other blogs | 8446 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Just tried it out - needs

Just tried it out - needs some serious user interface work:

"Feedback: This expression can be simplified. 'Feed' the leftmost argument into the leftmost λ-slot."

No indication of how to 'Feed' the argument in the user interface..

I think this project is just a command line shell; so just explain the syntax of the input files and explain how the output is formatted..

Just my 2cents; don't hate me;)

By ekoontz at Mon, 2007-07-23 02:04 | login or register to post comments

from one of the authors of the tool

Thanks for your comments. I realize we need to make the website clearer on what the tool does and does not offer.

This is *pedagogical* software developed for a specific context (university courses for students of formal semantics, mostly natural language semantics, a subfield of linguistics) -- it doesn't do lambda conversion for you. Instead it presents you with a number of lambda expressions and asks you to convert them by applying alpha and beta reduction where appropriate. You start up the tool, open an exercise file (there are two sample files available on the tool's website), and when it presents you a lambda term, you type in the reduced form of the term in the text box that says "enter an expression". Then on clicking "check answer" you get feedback from the tool.

The tool is definitely *not* a command line shell. The format of the exercise files is described on the website, http://www.ling.upenn.edu/lambda/exercisefiles.html.

There is a spec that will perhaps make the motivation for the tool clearer. http://www.ling.upenn.edu/lambda/spec.pdf

The underlying formalism is the simply typed lambda calculus.

By champoll at Wed, 2007-08-01 03:29 | login or register to post comments

Question

Other than representation, is a typed Lambda calculus really any different than a multi-sorted first-order logic (ie or predicate calculus) as a semantic representation?

By Hank Thediek at Mon, 2007-07-23 15:32 | login or register to post comments

Yes.

The types of a typed lambda calculus model propositions. The terms of a typed lambda calculus model proofs. So if you have (intuitionistic) first-order logic, then you can turn it into a type theory by giving the logical rules a proof term assignment -- ie, by associating a lambda term with each connective. This is useful for two reasons.

First, if your logic programming engine or theorem prover produces proof terms, you can debug it much more easily -- you can double-check the proofs to make sure they are correct. This is valuable even if all you care about is entailment.

Second, sometimes the specific proof you find matters. Concretely, imagine formalizing a planning problems. Here, we use a logical formula to represent a goal (ie, the desired state of affairs), and each proof we find is a plan for achieving that goal -- and different plans can require very different amounts of time and resources.

By neelk at Mon, 2007-07-23 17:09 | login or register to post comments