Abstract:
We study the structure of computations by term rewrite rules, allowing non-determinism and overlapping. Computations form, up to permutations of rewritings, a complete partial order, and semantics is defined as the set of results of terminating (i.e. maximal) computations. A call-by-need computation rule is then introduced and we prove, by means of a continuous projection over the complete partial order of call-by-need computations, that this rule is correct for sequential systems.