为什么lisp,或者说common lisp现在这么冷门呢?

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