Symbolic simplification of a program / exploring Gödel's Incompleteness theorem and the halting problem

.gitignore

node_modules

Readme.md

Program simplification / Halting problem

I wanted to play with some ideas after reading this article.

How to run

• Get a recent version of nodejs
• Install esprima (parser) with $ npm install esprima --save
• Run $ node simplify.js

The problem we are trying to solve

The article says Gödel's incompleteness theorem states:

The Incompleteness Theorem says that if your logical system can be used to represent arithmetic, then you can come up with a statement that you can neither prove nor disprove.

It seems like the reason for this is because it can be used to build self-referential constructs. If we had a sufficiently limited language that did not allow for this, then it would seem we could get around it.

I think that this means that our language cannot represent arithmetic, as my understanding of his completeness theorem is that he proved it by mapping numbers to strings so that he could then represent arbitrary text manipulation within arithmetic, which then allowed him to build self-referential programs, which then allowed him to construct the equivalent of "this statement is false".

If we could prevent the sentence from being able to refer to itself, then we wouldn't have this issue. At first, it seems like the lambda calculus has this constraint, but the y combinator shows that it does not. Really, referencability in general is the culprint.

The solution

The code here takes a program and simplifies it by inlining function invocations (because otherwise we must reference the function invocation). It works for the sample input, but probably not much else.

I ran it against an example program (in test.js) that recursively adds some numbers. I added unknownValue to show it actually simplifies the AST rather than evaluating the program (because this allows us to decide whether it can know enough to simplify the program down to a single value).

function countdown(n) {
  if(n == 0)
    return 0
  else
    return unknownValue + n + countdown(n-1)
}
countdown(3)

We can see that simplify.js handles our program as desired:

$ node simplify.js
Sanity check, set unknownValue 100, and let JavaScript eval it:
  306
Simplified program:
  'unknownValue + 3 + unknownValue + 2 + unknownValue + 1 + 0'
Simplified with initialScope: { unknownValue: '100' }:
  '306'

The problem with the solution

Some programs cannot be simplified like this because they recurse infinitely. Eg this program:

function countdown(n) {
  countdown(n)
}
countdown(3)

I'm ignoring that it explodes the callstack, I could define a more complex one that does not, but in the same way that we don't know whether the program halts, we don't know if the program would eventually converge, given a large enough callstack. So, lets assume we have an infinite callstack in order to ignore this uninteresting aspect of the problem.

In this case, our program would never converge as it need us to infinitely replace the function call with itself. Because this program diverges, we would like to say that it is illegal according to our constraints.

That implies that simplify.js should error out telling us that we cannot simplify our program because our program is illegal. So, simplify.js should be implemented like this:

if(illegal(program)) {
  process.stderr.write("Program is illegal\n")
  process.exit(1)
} else {
  // ... simplify the program ...
}

BUT!! How do we implement our illegal function? And that's the problem >.< illegal must know whether simplifying program will lead to infinite recursion, and thus never stop / cease / quit / conclude / halt... We've run into the halting problem!!

Alan Turing created the Turing Machine to prove that a program such as our illegal cannot exist for every input.

Proving the problem

Well, lets at least try to learn something. Lets say that we've figured out how to implement illegal in a way that will cause it to return true or false for any given program we could hand it. Then we could give it this program:

((src, q) => { if(illegal(src+'('+q+src+q+', '+'`'+q+'`'+')')) return 'fin'; else while(true) { }})("((src, q) => { if(illegal(src+'('+q+src+q+', '+'`'+q+'`'+')')) return 'fin'; else while(true) { }})", `"`)

It's a bit ridiculous in order to make it valid (I might have adhered to more constraints than were really necessary, also I could do this much simpler in Ruby) But the basic idea is that it reconstructs its own source code (this is called a quine), and then tests that. So it achieves self-referentiability by reconstruction of its source.

If we remove the annoying javascript cruft, we get this program:

if(illegal(thisSourceCode)) return 'fin'; else while(true) { }

So if our source code is illegal (it never halts), then illegal(thisSourceCode) returns true, so our program finishes by returning 'fin', hence it halts and hence it is legal. So if it says our program is illegal, then our program is legal.

Alternatively, if our source code is legal (it halts), then illegal(thisSourceCode) returns false, so our program goes into an infinite loop at while(true) { }, hence it does not halt and hence it is illegal, So if it says our program is legal, then our program is illegal.

No matter how it responds, illegal will be wrong, the program it is evaluating changes its behaviour based on illegal's analysis!

Conclusion

So, there are programs that we cannot determine if they are legal or not (if they halt or not), and thus have no way to take an arbitrary program and determine whether it can be converted to our restricted reference-free language.

simplify.js

'use strict'

const fs      = require('fs')
const program = fs.readFileSync("./test.js", 'utf8')
const inspect = toInspect => require('util').inspect(toInspect, {colors: true, depth: 10})

// sanity check, it evaluates correctly as JavaScript
{ let unknownValue = 100
  const jsResult = require('vm').runInNewContext(program, {unknownValue})
  console.log(`Sanity check, set unknownValue ${inspect(unknownValue)}, and let JavaScript eval it:`)
  console.log(`  ${inspect(jsResult)}`)
}

// now we symbolically replace it where we can
{ const JsAst      = require('esprima').parse(program)
  const simplified = simplify(JsAst, [{}])
  console.log(`Simplified program:`)
  console.log(`  ${inspect(simplified)}`)

  let unknownValue = '100'
  let initialScope = {unknownValue}
  const completelySimplified = simplify(JsAst, [Object.assign({}, initialScope)])
  console.log(`Simplified with initialScope: ${inspect(initialScope)}:`)
  console.log(`  ${inspect(completelySimplified)}`)
}

function simplify(ast, scopes) {
  switch(ast.type) {
    case "Program":
    case "BlockStatement":
      const exprs = ast.body.map(expr => simplify(expr, scopes))
      return exprs[exprs.length-1]
    case "FunctionDeclaration":
      scopes[scopes.length-1][getName(ast.id)] = ast
      return ast
    case "ExpressionStatement":
      return simplify(ast.expression, scopes)
    case "CallExpression":
      const fn       = lookup(getName(ast.callee), scopes)
      const args     = ast.arguments.map(arg => simplify(arg, scopes))
      const params   = fn.params.map(param => getName(param))
      const newScope = {}
      for(let index in params) newScope[params[index]] = args[index]
      return simplify(fn.body, scopes.concat(newScope))
    case "Literal":
      return ast.raw
    case "IfStatement":
      const test = simplify(ast.test, scopes)
      return simplify(ast[test==='true'?'consequent':'alternate'], scopes)
    case "BinaryExpression":
      const left  = simplify(ast.left,  scopes)
      const right = simplify(ast.right, scopes)
      switch(ast.operator) {
        case "==": return areComparable(left, right)   ? String(left == right)                : `${left} == ${right}`
        case "-":  return areSubtractable(left, right) ? String(Number(left) - Number(right)) : `${left} - ${right}`
        case "+":  return areAddable(left, right)      ? String(Number(left) + Number(right)) : `${left} + ${right}`
        default: throw(`Unknown operator: ${ast.operator}`)
      }
    case "Identifier":
      return lookup(getName(ast), scopes)
    case "ReturnStatement":
      return simplify(ast.argument, scopes)
    default:
      p(ast)
      throw `Unknown: ${ast.type}`
  }
}

function p(...objs) {
  objs.forEach(obj => console.dir(obj, {colors: true, depth: 5}))
}

function getName(ast) {
  if(typeof ast === "object" && typeof ast.name === "string")
    return ast.name
  p(ast)
  throw "NOT AN IDENTIFIER"
}

function lookup(name, scopes) {
  const [found, value] = scopes.reduceRight(
    ([found, val], node) => found ? [true, val] : node[val] ? [true, node[val]] : [false, val],
    [false, name]
  )
  return found ? value : name
}


function isBool(str) {
  return str === 'true' || str === 'false'
}

function isNumber(str) {
  return str.match(/^\d+$/) // good enough for our purposes for now, though obviously deficient
}

function areComparable(str1, str2) {
  if(isBool(str1) && isBool(str2)) return true
  if(areAddable(str1, str2)) return true
  return false
}

function areSubtractable(str1, str2) {
  return isNumber(str1) && isNumber(str2)
}

function areAddable(str1, str2) {
  return areSubtractable(str1, str2) // if we wanted to go further with this (we don't), we would allow strings to be added, as well
}

test.js

function countdown(n) {
  if(n == 0)
    return 0
  else
    return unknownValue + n + countdown(n-1)
}
countdown(3)