5109637047

Ewaluacja w porządku aplikatywnym (cali by value)

►    słaba postać normalna

v ::= \x.t \ x v\ ... v_n (n > 0)

►    relacja redukcji w porządku aplikatywnym —>_v

(Ax.t) v —t{v/x}

t —>_v t'    s —s'

t s —t_v t' s    v s —v s'

► relacja ewaluacji w stylu semantyki naturalnej

u{w/x} JJ^

t -lj-v Ax.u s w

X X Xx.t -IJ-jz Ax.t    t S v

(\/ / Ax.u)

t V s w

t S V w