Compute machine more powerful than Turing Machine

In this article, we describe a type of machine with more compute power than a Turing Machine.

Function definitions in most programming languages are compressed definitions. In other words, they are like syntax sugars.

Hypothetically, we have a type of machine called Machine Z that can turn the two functions below…

fn invert_1(x: bool) -> bool {
  if x == true {
    false
  } else {
    true
  }
}

fn invert_2(x: bool) -> bool {
  if x == false {
    true
  } else {
    false
  }
}

… into the mapping …

true -> false
false -> true

Then we say that invert_1 and invert_2 are definitionally equal, even though their notations in Rust are different.

In Machine Z, a function with type $A -> B$ is a set of paths¹, where, for all terms of $A$ ($a$), there exist a path whose start is $a$ and whose end is a term of $B$.

By this definition, how a function is described can be “compiled” into a mapping (a set of paths). To “apply a function”, is to apply the path with the function input as the path’s start.

noncomputable in Lean means “cannot be computed in a Turing Machine”, but some such functions can be computed in Machine Z.

In Machine Z, for any two functions of the same type, it’s possible to test if they are equal by reducing their description to mapping and compare the two mappings.