OBJ family 完全基于 reduction 和 term rewrite,立足于数学而独立于 Von Neumann 存在。
op nil : -> List .
op _._ : Qid List -> List
op length : List -> Nat .
op _in_ : Qid List -> Bool .
vars I J : Qid .
var L : List .
eq length(nil) = 0 .
eq length(I . L) = s length(L) .
eq I in nil = false .
eq I in J . L = (I == J) or (I in L) .
execution(reduction):
length(’a . ’b . ’c . nil)
= s length(’b . ’c . nil)
= s s length(’c . nil)
= s s s length(nil)
= s s s 0