Pf. Too convoluted. You have to define stuff in M expressions and then map them to S expressions. And what is it that you're defining? A set of primitive functions, some of them operating on specialised data structures. Why? Here's Prolog in Prolog:

  prove(true).
  prove((L,Ls)):-
      prove(L)
     ,prove(Ls).
  prove(L):-
      clause(L,Body)
     ,prove(Body).

  clause(H:-B,B).
  clause((H:-),true).

Also, rather fewer LOCs. LISP people are always bragging about their LOCs. I don't know why.

__________

[1] "SLDNF" Resolution is Selective Linear Definite Resolution with Negation as Failure, officially; or, Straight-up Logical Derivations with No Fuckups Resolution, as I prefer to think of it.

I feel a little sick every time I see this regurgitated; McCarthy's interpreter is not remotely in the same class as Maxwell's equations (and the Church-Turing thesis). It's neither axiomatic, universal, nor minimal. Good ol' lambda calculus does a much better job. For example, here's the lambda calculus self-interpreter [1]

  (\f. (\x.f(xx)) (\x.f(xx)) (\em.m(\x.x)(\mn.em(en)) (\mv.e(mv)))

Related:

“Maxwell's equations of software” examined (2008) - https://news.ycombinator.com/item?id=23321955 - May 2020 (47 comments)