5109637044

Ewaluacja w porządku normalnym (cali by name)

► słaba czołowa postać normalna

v ::= Xx.t \ x ti.. .t_n (n > 0)

► relacja redukcji w porządku normalnym —>_n

_ t —>n t'

(Ax.t) s —t{s/x} t s—>_n t's

► relacja ewaluacji jł„ w stylu semantyki naturalnej

V

tS jj„ V 5

X jłn X

t jj.„ Ax.u u{s/x) łj„ v

tS ii._n V

AX.t JJ-n Ax.t

(v ^ \x.u)