2
$\begingroup$

Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total languages]", to "show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter".

There has been some debate [1] over the precise definition of "interpreter" and "self-interpreter" within [0], and more broadly in the field. The general impression I draw from this discussion is that the "representation" and "reduction" of a program are a spectrum, with different evaluators performing different degrees of representation/reduction, partially dependent on the design of the evaluator, as bounded by the capabilities of the implementation language.

However, my question does not concern whether Brown and Palsberg's self-interpreter accomplishes interpretation, but instead whether and how their mechanism of forbidding diagonalization relates to other domains. As analogy, I appeal to Lawvere's Fixed Point Theorem (LFPT), which has been used to unify the presentation of a number of limitative theorems proven using diagonalization methods [2].

Can Brown and Palsberg's evasion of the effects of diagonalization be applied with similar breadth? Can their diagonalization-exclusion mechanism be translated to other diagonalization-based proofs? How does it stand with respect to the preconditions for the Fixed Point Theorem (e.g., does the LPFT simply not apply to the problem of total language self-interpretation)?

A further extension of this question would be to compare Brown and Palsberg's mechanism with Dan Willard's mechanism for avoiding diagonalization in his Self-Justifying Axiom Systems, as is asked in [3].

[0] http://compilers.cs.ucla.edu/popl16/

[1] http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/

[2] https://arxiv.org/abs/math/0305282

[3] Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

$\endgroup$
1
  • 1
    $\begingroup$ It's almost impossible to say anything intelligent about what Brown and Palsberg did without a definition of self-interpreter which includes their construction but excludes trivial self-interpreters for System T. Brown and Palsberg did not give one, and I do not know of one. $\endgroup$ Jun 11, 2022 at 21:33

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.