Copenhagen Programming Language
THE BETA CUBE
Álvaro García Pérez
IMDEA, Madrid, Spain
March 7th, 11:00 - 11:30
IT University of Copenhagen, Room 4A14
Pure lambda calculus reduction strategies have been thoroughly
studied, as they constitute the foundations of evaluation in many
programming languages. Sestoft collected and defined several of them
as sets of big-step rules, thus clarifying varying and inaccurate
definitions in the literature. From Sestoft's work, we present a rule
template which can instantiate any of the foremost strategies and some
more. Abstracting the parameters of the template, we propose a space
of reduction strategies we like to call the Beta Cube. We also
formalise a hybridisation operator--informally suggested by
Sestoft--which produces new strategies by composing a subsidiary and a
base strategy from the cube. Furthermore, we discuss a variant of the
hybridisation operator, in which the operand of an application is
reduced by the subsidiary instead of the hybrid. This accomplish with
the implicit remarks on Plotkin's theorems for the lambda-value
calculus. The new hybridisation operator allows to produce a
normalising strategy in Plotkin's (pure) lambda-value calculus.
This space gives new and interesting insights about the properties of
reduction strategies. We present and prove the Absorption Theorem,
which states that subsidiaries are left-identities of their hybrids.
This joint work with Pablo Nogueira and Emilio Jesús Gallego Arias is
available at http://iws2010.inria.fr/IWS2010-proceedings.pdf.
Peter Sestoft Administrative host:Renée Korver Michan.
All are welcome.
The Copenhagen Programming
Language Seminar (COPLAS) is a collaboration between DIKU,
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to
email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see