3 ms·
I think a meta-circular interpreter for Prolog would fit this description nicely. Prolog excels at writing interpreters in general, and in particular admits exc
by triska 3y ago
I think a meta-circular interpreter for Prolog would fit this description nicely. Prolog excels at writing interpreters in general, and in particular admits exceptionally short meta-circular meta-interpreters, i.e., interpreters written in Prolog that can interpret pure Prolog code, including their own source code.
An example of such a meta-circular Prolog interpreter is:
mi([]).
mi([G0|Gs0]) :-
clause(G0, Rs, Gs0),
mi(Rs).
It can interpret pure Prolog code, a Turing-complete subset of first-order predicate logic. For example, given the following clauses:
clause(natnum(0), Rs, Rs).
clause(natnum(s(X)), [natnum(X)|Rs], Rs).
It yields:
?- mi([natnum(X)]).
X = 0
; X = s(0)
; X = s(s(0))
; X = s(s(s(0)))
; X = s(s(s(s(0))))
; ... .
The meta-interpreter's own code can also be represented in this way:
clause(mi([]), Rs, Rs).
clause(mi([G0|Gs0]), [clause(G0,Rs,Gs0),mi(Rs)|Ls], Ls).
clause(clause(Head, Rs0, Rs), Ls, Ls) :- clause(Head, Rs0, Rs).
And now it can interpret its own source code, interpreting any given program, arbitrarily deeply nested. For example:
?- mi([mi([mi([natnum(X)])])]).
X = 0
; X = s(0)
; X = s(s(0))
; X = s(s(s(0)))
; ... .
Tested with Scryer Prolog.
- jabowery 3y agoIt would be interesting to see someone like Tromp explore binary FOL the way he's explored binary lambda calculus*. There are good reasons for going the FOL direction since functions are degenerate relations. While it is true that functional languages based on, for example, lambda or SK calculus, can naturally support "and parallelism" (eg x^2 in parallel with y^2 in x^2+y^2), getting "or parallelism" requires expression of independent processes (e.g.indeterminacy), some of which may not terminate. For example, operating systems need "or parallelism". *I'm not at all comfortable with Tromp's abandoning SK for lambda calculus in his search for a principled choice of UTM for Algorithmic Information Theory. His justification seems to be that lambda is "more expressive" than sk, but that begs the question: To express _what_?