## Abstract / Description of output

This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard's execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of λ-calculus [5].

The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one.

A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in [1]. But more efficient optimal implementations of λ-calculus are expected.

The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.

The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one.

A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in [1]. But more efficient optimal implementations of λ-calculus are expected.

The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.

Original language | English |
---|---|

Title of host publication | Computer Science Logic |

Subtitle of host publication | 10th International Workshop, CSL '96 Annual Conference of the EACSL Utrecht, The Netherlands, September 21–27, 1996 Selected Papers |

Editors | Dirk van Dalen, Marc Bezem |

Publisher | Springer Berlin Heidelberg |

Pages | 76-88 |

Number of pages | 13 |

Volume | 1258 |

ISBN (Electronic) | 978-3-540-69201-0 |

ISBN (Print) | 978-3-540-63172-9 |

DOIs | |

Publication status | Published - 1997 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 1258 |