Skip to content

Instantly share code, notes, and snippets.

@JakobBruenker
Last active July 1, 2023 15:13
Show Gist options
  • Save JakobBruenker/c0bed822fe1d840b15f83442bc8e77a3 to your computer and use it in GitHub Desktop.
Save JakobBruenker/c0bed822fe1d840b15f83442bc8e77a3 to your computer and use it in GitHub Desktop.
Roger's fixed-point theorem in Javascript
/*
Constructive proof of Roger's fixed-point theorem in Javascript
===============================================================
N.B. You can load this file in node.js using `.load roger.js` to use the
functions defined here in a REPL.
Definition (Program)
--------------------
Below, a "program" will always be a Javascript function of one argument.
Definition (Gödel number)
------------------------
A Gödel number is a serialized representation of a Turing machine (typically in
form of a natural number) or, equivalently, the source code of a prorgam, in
form of a string
Definition (φ)
--------------
φ is a function that turns a Gödel number into the corresponding Turing machine -
or turns source code into a program.
Definition (fixed point)
------------------------
Given a function F, a fixed point of F is a Gödel number n such that φ(n) = φ(F(n)).
Theorem (Roger's fixed-point theorem)
-------------------------------------
If F is a total computable function, it has a fixed point in the above sense.
"total" means it produces a value for every possible input, and "computable"
means it can be represented by Javascript source code. We will exploit this by
using Javascript's functionality to get a function's source code by using
`.toString()`. If we didn't have this, we could require passing in the source
code as argument instead of passing in the function.
The proof given here mirrors the one given at
https://en.wikipedia.org/wiki/Kleene%27s_recursion_theorem#Rogers's_fixed-point_theorem
(More precisely, this implements the construction given in the proof -
we're not actually checking here whether that construction is a valid proof.)
Javascript is one language particularly suitable for this because we don't have to implement our own φ - it's buil-in, in the form of `eval`. While `eval` might seem like cheating, it is perfectly possible to implement a Javascript interpreter in Javascript without using `eval` - it's just a lot more work.
*/
// This function is not necessary, but just serves as a sanity check to make
// sure we're not doing something stupid
function checkType(type, input) {
if (typeof input === type) {
return input
} else {
throw new Error(`${input} is not a ${type}!`)
}
}
const φ = input => eval(checkType('string', input)) // interpret string as javascript program
const phi = φ // ASCII variant for those of us outside of Greece
const q = JSON.stringify // quote a string
const g = a => a.toString() // Gödel number/source code
// Given an input x, h constructs a string representing the program
// "Given an input y, see what φ(x)(x) does.
// If it throws an error or runs forever, do the same.
// If it produces a result r, return Φ(r)(y)."
const h = x => `(y => φ(φ(${q(x)})(${q(x)}))(y))`
const fixedPoint = F => {
// e is a string representing the program F ∘ h
const e = `(x => φ(${q(g(F))})(h(x)))`
// We can prove that a fixed point exists by seeing that
//
// 1. φ(h(e)) = (y => φ(φ(e)(e))(y)) (definition of h)
// = φ(φ(e)(e)) (eta reduction)
//
// 2. e = g(F ∘ h) (definition of e)
//
// 3. φ(e)(e) = φ(g(F ∘ h))(e) (x => φ(x)(e) applied to both sides of 2.)
// = (F ∘ h)(e) (definition of φ)
// = F(h(e)) (definition of ∘)
//
// 4. φ(φ(e)(e)) = φ(F(h(e))) (φ applied to both sides of 3.)
//
// 5. φ(h(e)) = φ(F(h(e))) (transitivity on 1. and 5.)
//
// But this matches exactly our definition of a fixed point for n = h(e).
// Thus, h(e) is a fixed point for F. ∎
return h(e)
}
/*
For a given function F: string -> string, `fixedPoint` produces a string s
such that
φ(s) = φ(F(s))
For most functions F, the function that s represents will simply be a function
that is nowhere defined, and instead throws a runtime error for every possible
input. This is because most functions typically don't produce valid Javascript
code when applied to any string.
For example:
φ(fixedPoint(x => ''))(13) ==> Uncaught TypeError: φ(...) is not a function
φ(fixedPoint(x => x + '!'))(13) ==> Uncaught SyntaxError: Unexpected token '!'
φ(fixedPoint(x => x + ';'))(13) ==> Uncaught RangeError: Maximum call stack size exceeded
Note that in all of these examples, the theorem is still true, e.g.
φ(fixedPoint(x => x + '!')) = ф(fixedPoint(x => x + '!') + '!')
(Note the extra '!' on the right-hand side.)
The error message will be the same for both of these functions.
You might be wondering what the actual fixed point looks like. Using the second example again, we get
fixedPoint(x => x + '!') ==>
`(y => φ(φ("(x => φ(\\"x => x + '!'\\")(h(x)))")("(x => φ(\\"x => x + '!'\\")(h(x)))"))(y))`
There are, however, some functions that produce more interesting behaviors.
This includes in particular functions that convert any string into a valid
Javascript program, where a valid Javascript program is one that evaluates to a
function of one argument.
Trivial examples
================
Possibly the most simple example is something like
fixedPoint(x => 'y => 42')
This will produce a string representing a function that always returns 42:
φ(fixedPoint(x => 'y => 42'))(13) ==> 42
Sticking with ignoring the first argument, we can try returning the second one unchanged, as in
fixedPoint(x => 'y => y')
This will result in φ(s) being the identity function, since
φ(s) = φ(F(s)) = φ('y => y') = (y => y)
Another example is F(x) = 'a => ' + x, which will result in s representing a
curried function that takes an infinite number of arguments:
φ(s) = φ(F(s)) = φ('a => ' + s)
s = 'a => a => a => a => ...'
Note that this will not actually be what the string s looks like, since
infinitely long strings are not allowed in Javascript. The actual result of
`fixedPoint(s => 'a => ' + s)` will be
`(y => φ(φ("(x => φ(\\"s => 'a => ' + s\\")(h(x)))")("(x => φ(\\"s => 'a => ' + s\\")(h(x)))"))(y))`
A more interesting example
==========================
It turns out that `F => φ(fixedPoint(F))` actually has more or less the same
behavior as the Y combinator, and thus we can use it to implement any
computable function if we are smart about choosing F.
We do this via a straightforward translation from a standard recursive
function. For example, let's say we have this function for computing
factorials:
const fact = n => n === 0 ? 1 : n * fact(n - 1)
We can produce the same function with our fixed point construction by writing
const fact = φ(fixedPoint(fact => `n => n === 0 ? 1 : n * ${fact}(n - 1)`))
The notable difference is that this function isn't recursive - instead, the
function is its own argument, and we can exploit that fact to emulate what
recursion would do.
(Though of course we would need something like recursion if we wanted to
implement `eval` ourselves.)
Example:
φ(fixedPoint(fact => `n => n === 0 ? 1 : n * ${fact}(n - 1)`))(6) ==> 720
*/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment