 Summary
|
The thesis addresses the issue of defining models to
implement the beta-reduction in the
lambda-calculus. We focus especially on two kinds
of models: explicit substitution calculi, and interaction
nets.
-
Explicit substitution calculi are studied in
several contexts. On the one hand, they are studied in the
context of automatic provers, where it is interesting to
have a calculus which is both confluent on terms with
first-order variables and preserving strong
normalization. These properties would allow for the
representation of incomplete proofs. We discuss these
properties, and give important contributions to an open
problem in this field. On the other hand, explicit
substitution calculi are applied to functional programming
and weak reduction which is its fundamental concept. It is
then essential to have tools which can express the sharing
provided by implementations, particularly for lazy
languages. To illustrate this, we give a very precise and
formal proof of the correctness of KP, an abstract machine
for lazy reduction of the lambda-calculus, using a
calculus of explicit substitution and global adresses,
namely lambda-sigma-w-a. We then propose an
optimization for this machine.
Interaction nets are usually associated to optimal
reduction à la Lévy, as described by
Lamping's algorithm. However, this algorithm is known as
rather complex. We study in our thesis a reducer based on
some ideas due to Lamping, but leaving out some
constraints introduced for optimality. Thus, we obtain a
non optimal algorithm that we compare to Lamping's
algorithm (implementation of Asperti) and KP. The results
show as expected that our algorithm provides quite a good
amount of sharing, without the bureaucracy that one finds
in optimal interpreters.
|
Thesis