External and internal syntax of the lambda-calculus

Masahiko Sato, from SCSS 2009, available from Masahiko Sato’s webpage:

It is well known that defining the substitution operation on λ-terms appropriately and establish basic properties like the substitution lemma is a subtle task if we wish to do it formally. The main obstacle here comes from the fact that unsolicited capture of free variables may occur during the substitution if one defines the operation naively.

We argue that although there are several approaches to cope with this problem, they are all unsatisfactory since each of them defines the λ- terms in terms of a single fixed syntax. We propose a new way of defining λ-terms which uses an external syntax to be used mainly by humans and an internal syntax which is used to implement λ-terms on computers.

In this setting, we will show that we can define λ-terms and the substitution operation naturally and can establish basic properties of terms easily.

Slides from a talk covering related work with Randy Pollack, presented at TAASN 2009, are available from Randy Pollack’s website.

0 Responses to “External and internal syntax of the lambda-calculus”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: