Strict  versus  lazy  evaluation

Mircea Marin

In functional programming, we can define a function f by conditional rewrite rules

f[(Subscript[s, 1]), ..., (Subscript[s, m])] -> r ⟸ (Subscript[L, 1]) && … && (Subscript[L, n])

where the conditions (Subscript[L, o]) are formulas (Subscript[l, i]) (SuperStar[->]) (Subscript[r, i]) with the informal reading that (Subscript[r, i]) is the value of (Subscript[l, i]). A functional program is a finite set R of conditional rewrite rules, called conditional term rewriting system (CTRS). A CTRS induces a rewrite relation (Subscript[->, R]) which is defined as follows: s(Subscript[->, R])t holds if there exist a context C and a conditional rewrite rule

l -> r ⟸ ((Subscript[l, 1])(SuperStar[->])(Subscript[r, 1])) && … && ((Subscript[l, n])(SuperStar[->])(Subscript[r, n]))

such that s=C[u], t=C[v], and there is a substitution σ such that σ(l)=u, σ(r)=v, and σ((Subscript[l, i]))(Subscript[->, R]^( * ))σ((Subscript[r, i])) for all 1≤i≤n.

Some natural assumptions

A natural restriction on functional programs is to assume that its rules l -> r ⟸ ((Subscript[l, 1])(SuperStar[->])(Subscript[r, 1])) && … && ((Subscript[l, n])(SuperStar[->])(Subscript[r, n])) satisfy the following syntactic restriction, which we call admissibility:

Admissibility allows to perform conditional rewrite steps by a sequence of matching operations: If s∈T(F,∅) and l -> r ⟸ ((Subscript[l, 1])(SuperStar[->])(Subscript[r, 1])) && … && ((Subscript[l, n])(SuperStar[->])(Subscript[r, n])) then the search for a term t such that  s(Subscript[->, R])t holds cam be done as follows:

Another natural assumption is to assume that every term (Subscript[t, i]) is an R-normal form, that is, there is no term (Subscript[u, i])∈T(F,∅) such that (Subscript[t, i])(Subscript[->, R])(Subscript[u, i]). A value of a ground term which is irreducible.

Conditional term rewriting with RhoLog

In this section we show how we can use RhoLog for conditional term rewriting. The ideas is simple: we view every conditional rewrite rule

f[(Subscript[s, 1]), ..., (Subscript[s, m])] -> r ⟸ ((Subscript[l, 1])(SuperStar[->])(Subscript[r, 1])) && … && ((Subscript[l, n])(SuperStar[->])(Subscript[r, n]))

of a CTRS R as a defining rule for function symbol f:

f[(Subscript[s, 1]), ..., (Subscript[s, m])] (Subscript[->, "R"]) r ⟸ ((Subscript[l, 1])(Subscript[->, "NF"["Rw"["R"]]])(Subscript[r, 1])) && … && ((Subscript[l, n])(Subscript[->, "NF"["Rw"["R"]]])(Subscript[r, n]))

Then s(Subscript[->, R])t holds if s(Subscript[->, "Rw"["R"]])t holds.

Case study: Peano  arithmetic

In Peano arithmetic, a natural number is either 0 or the successor s[n] of a natural number n. Addition and multiplication can be defined by the CTRS

{0⊕x->(x^i),x⊕0->(x^i)s[x]⊕s[y]->s[s[x⊕y]],0⊗x->0,x⊗0->0,s[(x^i)]⊗s[(y^i)]->(((x^i)⊗(y^i))⊕((x^i)⊕(y^i)))⊕s[0]}

The RhoLog specification of this CTRS is:

<<RhoLog`
DeclareRules[
0⊕(x^i)(Subscript[->, "R"])(x^i),
(x^i)⊕0(Subscript[->, "R"])(x^i),
s[(x^i)]⊕s[(y^i)](Subscript[->, "R"])s[s[(x^i)⊕(y^i)]],
0⊗((_)^i)(Subscript[->, "R"])0,
((_)^i)⊗0(Subscript[->, "R"])0,
s[(x^i)]⊗s[(y^i)](Subscript[->, "R"])(((x^i)⊗(y^i))⊕((x^i)⊕(y^i)))⊕s[0]
]

For example, we can use RhoLog to rewrite the term

t = (s[0]⊗(s[s[0]]⊕s[0]))⊗(0⊕s[0])

with our CTRS, any number of times:

(* One rewrite step *)
ApplyRule["Rw"["R"],t]

returns the result of rewriting t by applying the rule s[(x^i)]⊕s[(y^i)](Subscript[->, "R"])s[s[(x^i)⊕(y^i)]] to the subterm s[s[0]]⊕s[0] of  t.

(* A sequence of two rewrite steps *)
ApplyRule["Repeat"["Rw"["R"],2],t]

(* A sequence of 6 rewrite steps *)
ApplyRule["Repeat"["Rw"["R"],6],t]

(* A sequence of 7 rewrite steps *)
ApplyRule["Repeat"["Rw"["R"],7],t]

(* A normalizing computation *)
ApplyRule["NF"["Rw"["R"]],t]

It can be verified that blind rewriting finds the value s[s[s[0]]] of t after 15 rewrite steps:

{ApplyRule["Repeat"["Rw"["R"],14],t],ApplyRule["Repeat"["Rw"["R"],15],t]}

Evaluation strategies for Functional Programming

Functional programming languages don’t compute values by blind normalization of terms, but implement certain evaluation strategies.

Strict evaluation

Strict functional languages normalize term with the “Inner”[“R”] strategy. For example, the term

t2=(0⊗(s[s[0]]⊕s[0])⊕s[0])⊗(0⊕s[0])

has normal form s[s[0]]:

ApplyRule["NF"["Rw"["R"]],t2]

We can use RhoLog to check that there are 288 ways to compute a normal form of t2, which is unique: s[0].

Length[t2Vals=ApplyRuleList["NF"["Rw"["R"]],t2]]

t2Vals

Strict functional languages normalize terms with the “Inner”[“R”] strategy:

(* Strict evaluation of t2*)
ApplyRule["StrictEval"["R"],t2]

This value is found by a refutation of length 10:

(0⊗(s[s[0]]⊕s[0])⊕s[0])⊗(0⊕s[0])->(0⊗s[s[s[0]⊕0]]⊕s[0])⊗(0⊕s[0])->(0⊗s[s[s[0]]]⊕s[0])⊗(0⊕s[0])->(0⊕s[0])⊗(0⊕s[0])->s[0]⊗(0⊕s[0])->s[0]⊗s[0]->(0⊗0⊕(0⊕0))⊕s[0]->(0⊕(0⊕0))⊕s[0]->(0⊕0)⊕s[0]->0⊕s[0]->s[0]

We can use RhoLog to check this fact:

Table[ApplyRule["Repeat"["Inner"["R"],n],t2],{n,0,10}]

Notice that strict evaluation is still nondeterministic because a term can have many innermost “R”-redexes. In particular, there are 80 ways to compute the value of t2 by strict evaluation.

ApplyRuleList["StrictEval"["R"],t2]//Length

Lazy evaluation

Lazy functional languages normalize terms with the “Outer”[“R”] strategy:

(* Lazy evaluation of t2*)
ApplyRule["LazyEval"["R"],t2]

This value is found by a refutation of length 8:

(0⊗(s[s[0]]⊕s[0])⊕s[0])⊗(0⊕s[0])->(0⊕s[0])⊗(0⊕s[0])->s[0]⊗(0⊕s[0])->s[0]⊗s[0]->(0⊗0⊕(0⊕0))⊕s[0]->(0⊕(0⊕0))⊕s[0]->(0⊕0)⊕s[0]->0⊕s[0]->s[0]

We can use RhoLog to check this fact:

Table[ApplyRule["Repeat"["Outer"["R"],n],t2],{n,0,8}]

Notice that lazy evaluation is still nondeterministic because a term can have many outermost “R”-redexes. In particular, there are 24 ways to compute the value of t2 by lazy evaluation.

ApplyRuleList["LazyEval"["R"],t2]//Length