Notes
2025/09/20
Continuing last week's thoughts about paradoxical solutions for recursive loops that show similarities to the halting problem, here are a couple of “test cases” that any attempted solution should be able to handle.
The following code snippets all assume that the language provides some kind of paradoxical values, such as "x" & "y", which are both "x" and "y" at the same time. When the paradoxical value "x" & "y" is compared to the normal value "x" using an if-then-else construct, the paradoxical value matches both the then-branch and the else-branch.
What this means in practice depends on the implementation and on the logical laws that govern the behavior of paradoxical values.
If paradoxical values are part of the language and can be referred to from within the language (as opposed to being constructs in some meta language), it is possible to compare a paradoxical value against another (syntactically equivalent) paradoxical value:
v = "x" & "y"
if v == ("x" & "y"):
a
else:
b
If two paradoxical values are compared using some form of distributive law, it must be guaranteed that the comparison of two syntactically equivalent values simply evaluate to being true. In other words, the comparison of two equivalent paradoxes must not lead to a paradox:
# this should always evaluate to `x`
if v == v:
x
else:
y
With that out of the way, let's look at a few test cases that involve recursive loops:
The whole reason for introducing paradoxical values is that we want to be able to reason about self-referential expressions that resemble the liar's paradox:
# should lead to a paradox like "x" & "y"
def f():
if f() == "x":
"y"
else:
"x"
But if paradoxical values can be named in the language, it becomes possible to “capture” a paradox and then return a non-paradoxical value. A valid prediction must thus be “stronger” than just "x" & "y":
def f():
if f() == ("x" & "y"):
"y"
else:
"x"
Here's another variant, which embeds the liar in the else-branch of the captured liar. If "x" & "y" is a valid prediction for the liar, a stronger prediction is necessary for this case, because "x" & "y" would just return the non-paradoxical "x". A prediction for such a strengthened liar must thus be stronger than "x" & "y" without collapsing back into "x" & "y".
def f():
if f() == ("x" & "y"):
"x"
else:
if f() == "x":
"y"
else:
"x"
Like the above, but returning a different value in case the liar is captured:
def f():
if f() == ("x" & "y"):
"z"
else:
if f() == "x":
"y"
else:
"x"
Now we come to a few equivalences that should hold even in the presence of paradoxes. We often reason about conditionals by analyzing the cases, inferring that in the else-branch of if v == "x": ... else: ... the value v can never be equal to "x". This should be preserved in the presence of paradoxical values v which could be both "x" and not "x".
# f should be identical to the following:
#
# def f():
# if f() == "x":
# "y"
# else:
# "x"
#
def f():
if f() == "x":
"y"
else:
if f() == "x":
"y"
else:
"x"
Like the above, but returning a different value in the nested then-branch:
# f should be identical to the following:
#
# def f():
# if f() == "x":
# "y"
# else:
# "x"
#
def f():
if f() == "x":
"y"
else:
if f() == "x":
"z"
else:
"x"
Lastly, if paradoxical values are meant to be the fixed points of loops, we come to the question of how different paradoxical values interact without breaking referential transparency, in other words, without breaking the guarantee that variables can be freely substituted for their values and vice versa.
For example, let's consider the following function:
def f():
g = f
if f() == "x":
"y"
else:
if g() == "x":
"z"
else:
"x"
Since g is equal to f, the function should never return "z", because whenever g() == "x" it is also the case that f() == "x", so "y" should be returned. This would allow us to simplify the above to the following:
def f():
if f() == "x":
"y"
else:
"x"
This is just the liar, so it should evaluate to the paradoxical value "x" & "y". But if we now take this value for f() and substitute it in the code snippet that we started with, we get the following:
def f():
if ("x" & "y") == "x":
"y"
else:
if ("x" & "y") == "x":
"z"
else:
"x"
But this is clearly not equal to the liar, because the inner conditional would evaluate to "x" & "z":
def f():
if ("x" & "y") == "x":
"y"
else:
"x" & "z"
The lesson here is that we need to be careful how we substitute equal values in the presence of recursion, because fixed points implicitly have a notion of “scope” due to being recursive.