Advertisement
Published in:
2005 | OriginalPaper | Chapter
Call-by-Value Is Dual to Call-by-Name – Reloaded
Author : Philip Wadler
Published in: Term Rewriting and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We consider the relation of the dual calculus of Wadler(2003) to the
λμ
-calculus of Parigot (1992). We give translations from the
λμ
-calculus into the dual calculus and back again. The translations form an equational correspondence as defined by Sabry and Felleisen (1993). In particular, translating from
λμ
to dual and then ‘reloading’ from dual back into
λμ
yields a term equal to the original term. Composing the translations with duality on the dual calculus yields an involutive notion of duality on the
λμ
-calculus. A previous notion of duality on the
λμ
-calculus has been suggested by Selinger (2001), but it is not involutive.
Note:
This paper uses color to clarify the relation of types and terms, and of source and target calculi. If the URL below is not in blue please download the color version from
$$ \texttt{http://homepages.inf.ed.ac.uk/wadler/} $$
or google ‘wadler dual reloaded’.