Notes
2025/09/28
This continues the exploration from last week about a calculus for dealing with paradoxical solutions for recursive loops. This week's note focuses on how time loops are shifted to achieve true fixed points and walks through a few concrete examples of paradoxical solutions.
Last week's sketch left us with an important gap: our proposed time loops weren't quite fixed points because function application would shift them. ['x'; 'y'] would become ['y'; 'x'] after applying our liar function, giving us the right pattern but shifted by one position.
The key insight is that time loops need to track both their current step and their phase. Each time the time loop is applied to a value, it counts as a step. The phase is fixed and specifies after how many steps a time loop is shifted by one position. The notation ['x'; 'y']@0/2 represents a time loop at step 0 with a phase of 2.
Concretely, shifts can happen when a time loop is used as an argument or as a function:
“Normal” values have a phase of 0, which just means that they are never shifted in either direction. If the phase is 0, the step-and-phase annotation is omitted.
This shifting mechanism ensures that after a complete function application cycle, we get back to the original time loop configuration, returning true fixed points rather than shifted versions.
Let's examine how this works with concrete examples from our implementation.
if ['x'; 'y']@0/2 == 'x':
'y'
else:
'x'
The time loop ['x'; 'y']@0/2 represents our paradoxical value. At step 0, it's 'x', so the comparison ['x'; 'y'] == 'x' evaluates to [true; false]@0/2. The conditional then applies the time loop to two arguments, which increments the step counter twice and returns 'y' for the first case and 'x' for the second, giving us ['y'; 'x']@2/2. After shifting, this becomes ['x'; 'y']@0/2 again, which is what we started with and thus a fixed point.
if [['x']; ['y'; 'x']]@0/2 == ['x'; 'y']:
'y'
else:
'x'
Here we have a depth-2 time loop being compared to a depth-1 time loop. Since the depths differ, the comparison lifts the smaller depth value. The first element ['x'] gets compared to the entire ['x'; 'y'], yielding [true; false]. The second element ['y'; 'x'] also gets compared to ['x'; 'y'], yielding [false; false]. This gives us the nested boolean [[true; false]; [false; false]]@0/2, which simplifies to [[true; false]; [false]]@0/2.
The conditional then applies this time loop to the arguments 'y' and 'x'. After two applications, the step counter reaches 2, returning [['y'; 'x']; ['x']]@2/2. Since step equals phase, this triggers a shift that rotates the result and resets to step 0, giving us our original [['x']; ['y'; 'x']]@0/2.
if [['x']; ['x'; 'y']]@0/2 == ['x'; 'y']:
'x'
else:
if [['x']; ['x'; 'y']]@0/2 == 'x':
'y'
else:
'x'
This example shows how nested conditionals can “escape” certain paradoxical patterns. At the first level, ['x'] compared to ['x'; 'y'] gives [true; false], while ['x'; 'y'] compared to ['x'; 'y'] gives [true; true]. The outer condition evaluates to [[true; false]; [true]]@0/2, selecting 'x' in the true case and entering the inner conditional in the false case.
The comparison of the inner conditional evaluates to [[true]; [true; false]]@0/2, which is applied to the two arguments 'y' and 'x', leading to [['y']; ['y'; 'x']]@2/2. This is now shifted, so that the inner conditional evaluates to [['y'; 'x']; ['y']]@0/2.
When the value [[true; false]; [true]]@0/2 from the outer conditional is applied to the evaluated result of the inner conditional, the inner conditional is shifted back (because it is used as an argument), so that [[true; false]; [true]]@0/2 is zipped together with x (from the outer then-branch) and [['y']; ['y'; 'x']]@2/2, evaluating to [[true('x', 'y'); false('x', 'y')]; [true('x', 'x')]]@2/2, which finally evaluates to the shifted value [['x']; ['x'; 'y']]@0/2.
The synchronization of time steps ensures that the inner conditional is only visited when the outer condition is false, preventing any interference between the nested paradoxes.
if ['x'; 'y']@0/2 == 'x':
'y'
else:
if ['x'; 'y']@0/2 == 'x':
'y'
else:
'x'
This demonstrates the compositional nature of time loops. Even though the same time loop ['x'; 'y']@0/2 appears in multiple places, the synchronized time steps ensure consistent behavior. At step 0 (when the value is 'x'), both comparisons yield true, so only the outer then-branch executes, returning 'y'. At step 1 (when the value is 'y'), both comparisons yield false, so we enter the outer else-branch and then the inner else-branch, returning 'x'.
The result is ['y'; 'x']@2/2, which after shifting becomes ['x'; 'y']@0/2, which is exactly what we started with. The middle branch (inner then-branch) is never visited because the conditions are always synchronized.
The time loop calculus provides a systematic way to reason about paradoxical fixed points while maintaining compositional semantics. The shifting mechanism ensures that we get true fixed points rather than approximate ones, and the depth-based lifting rules allow us to combine different paradoxical subexpressions without interference.
The synchronization of time steps across all uses of a time loop value allows us to analyze complex nested conditionals by considering each time step independently, then combining the results into a unified time loop solution.
Future work might explore how this approach scales to more complex programming constructs and whether similar techniques can be applied to other forms of self-reference beyond the boolean paradoxes examined here.