1st Semester 2003/04: Reclose and Reopen

Instructors

dr Vincent van Oostrom; e-mail: Vincent.vanOostrom@phil.uu.nl; prof. dr Albert Visser; e-mail: Albert.Visser@phil.uu.nl

ECTS

6

Description

Any calculus having binding constructs, such as predicate calculus or the lambda-calculus, brings the notion of scope with it. Approaches on how to deal with scoping can be found in [1] and [2]. A common feature of both approaches is to treat scoping of variables by means of stacks (roughly, the top of the stack corresponds to the current occurrence of a variable having scoping effect). A distinguishing feature is that in the former approach every variable has its own stack (multi-stack), while in the latter all variables share the same stack (uni-stack).

The project is to investigate whether both approaches can be unified. In particular, whether the uni-stack approach to the extension of the lambda-calculus with an explicit end-of-scope operator in [2], can be changed into a multi-stack approach. The idea is that the introduction of another operator, the reopen-scope, suffices, if at the same time the semantics of the end-of-scope is changed into a reclose (reversible close). The question is, does this idea work, in particular, can beta-reduction be extended in a suitable way?

Since this is a rather technical project, knowledge of stacks (in any form, be it as stacks in formal language theory, or data types, or dynamic semantics) and the lambda-calculus is required. A good test is your ability to understand the issues raised and solved in [2].

Organisation

Meeting frequency: 2 hours per week

Location: The project will take place in Utrecht.

References

[1] Hollenberg, M. and Vermeulen, C.F.M., Counting Variables in a Dynamic Setting, Journal of Logic and Computation 6(5), 725-744, 1996.
[2] Hendriks, R.D.A. and van Oostrom, V., Adbmal, CADE 19, Lecture Notes in Artificial Intelligence 2741, 136 - 150, 2003.