Record number :

16861

Title of article :

Controlled Temporal Non-Determinism For Reasoning With A Machine Of Finite Speed

Author/Authors :

Ennals، Robert نويسنده ,

Issue Information :

روزنامه با شماره پیاپی سال 1999

Pages :

-338

From page :

339

To page :

0

Abstract :

In this paper we present a non-deterministic call-by-need (untyped) lambda calculus (lambda)nd with a constant choice and a let-syntax that models sharing. Our main result is that (lambda)nd has the nice operational properties of the standard lambda calculus: confluence on sets of expressions, and normal order reduction is sufficient to reach head normal form. Using a strong contextual equivalence we show correctness of several program transformations. In particular of lambdalifting using deterministic maximal free expressions. These results show that (lambda)nd is a new and also natural combination of non-determinism and lambda-calculus, which has a lot of opportunities for parallel evaluation. An intended application of (lambda)nd is as a foundation for compiling lazy functional programming languages with I/O based on direct calls. The set of correct program transformations can be rigorously distinguished from non-correct ones. All program transformations are permitted with the slight exception that for transformations like common subexpression elimination and lambda-lifting with maximal free expressions the involved subexpressions have to be deterministic ones.

Keywords :

level-order , co-induction , breadth-first , traversal , unfold , functional programming , anamorphism , fold , Program calculation

Journal title :

A C M Sigplan (Programming Languages) Sigplan Notices

Link To Document :