(1) The other is Church’s lambda calculus
(1) The other is Church’s lambda calculus
There's some understanding that I'm fundamentally lacking which I've been searching to correct for years. I've put it down to "Math" which seems to be a whole impenetrable language itself. A language that my lack of understanding of (despite many unguided attempts) means I'll continue to be downvoted and snorted at when I say I still don't understand what a Turing machine or a monad actually is.
Probably the most visible outcomes of this work is complexity analysis of algorithms- you can’t talk about how much computational effort you need to do something until you have an agreed measure of computational effort. How many steps or tape cells a Turing machine would need is that fundamental measure, in a similar way to how the speed of light is our fundamental measure of velocity; they’re essential to our understanding of the field but not used on a day-to-day basis. Instead, we use more convenient ones that are themselves derived from the first-principles units.
> Young man, in mathematics you don't understand things. You just get used to them.
This was John von Neumann talking.
And yes, mathematics is a language; it is the language for modelling the phenomena we experience in the world, including the non-physical (contracts, data / counting, etc.).
I so, so, so wish that people were taught that mathematics is a language of relationships rather than one of rote numerical calculation. I think more people would stick with it. It's a shame, because the doors it opens are huge.
Slightly longer answer: To the extent that they are formal languages, they both have the same ability to express things.
More philosophical answer: Mathematics has a tradition of extension. Have a new idea you want to express as concisely as possible because you are going to be using it a lot? Grab a handful of Greek letters, symbols, funny fonts, and random other typography, and go to town. Outside of Lisp,[1] this flexibility is hard to do in most programming languages.
[1] But inside a dog, it's too dark to read.
The long(er) answer? Mathematics are more limited, and thus, at least on the surface, provide a more rigid model.
Plus, we have about 4500 years worth of equations that we know to be accurate; not so true for C or any other programming language. Plus, we can model all the way down in mathematics, as it is more abstract in nature.
The long(est) answer? It's turtles all the way down.
The fundamental point of the Church-Turing thesis is to show that everything computers can do can be described by mathematics, so any programing language has either the same or less power than math. They are certainly easier to use for many problems, though.
Additionally, Gödel showed that there are true statements that can be described but not proven by math, ao it can never be a perfect model of the real world.
I assume you are refering to Gödel's incompleteness theorems; but this is not what they "say".
What they say is that any formal system powerful enough to contain basic arithmetic is either inconsistent (ie. it can both prove and disprove a particular theorem) or incomplete (ie. cannot either prove or disprove all theorems).
If you take the ZF set theory, for example, it is incomplete, because some statements cannot be either proved or disproved within ZF, such as the Axiom of Choice (AC) or Zorn's Lemma.
However, that doesn't imply that ZF cannot be "a perfect model of the real world", because the AC is irrelevant in a the real world, because the AC only applies to infinite sets, which do not exist in the real world.
As with many other interfaces, there are a few rules in the comments that implementations are expected to adhere to.
Consider the notion of an algorithm. You are probably familiar with an algorithm: a series of steps to be completed by a computer (aka a person).
This is the launch point for what a Turing machine is. Turing asks the question: if there exists a machine that can slavishly follow instructions, what can such a machine do, and what can such a machine NOT do?
To answer this question without invoking the AI problem, Turing started with the simplest possible set of objects to work with: binary numbers. A simple machine then would be a machine that reads a "tape" of binary numbers. The machine is simple, so it can only read one number at a time. Based on the number read, the machine may either move the tape left (reading the next number), move the tape right (read the previous number), replace the digit on the current cell, or halt.
You can see why such a machine is considered simple: The range of inputs and the action space is VERY limited.
And yet despite its simplicity, it's shown that such a simple machine can do addition. Specifically it can perform computation on recursively enumerable problems. It is in this very narrow and specific sense that Church's Lambda Calculus and Turing's machines are considered equivalent. Modern authors tend to extend the reach of Lambda Calculus, but you should bear in mind that the Church Turing thesis is valid only for functions N->N. That is to say if a Turing Machine can calculate the result of a function that takes a natural number and returns a natural number, lambda calculus can calculate the same result, and vice versa [sidenote].
Now, having a machine that can do all that is pretty cool. Ideally you'd want to be able to describe the rules of the machine. That's called a programming language. This notion really only formalized itself way after Turing died. Aho, Ulman and gang were really the ones who made the connection between languages and automata. Wang's B machine introduced the notion of abstraction in Turing machines by adding compound features that can be translated to simple Turing machines (for example, an instruction that would be "delete the value, and move right"). This led to the study of programming languages. The family of imperative programming languages are inspired by Turing machines in this manner.
[Sidenote]: If only functions of N->N are comparable for the Church Turing thesis, then why do people generalize it to all kinds of functions? A cheap trick is to say, all functions can be Gödel-string encoded. A G-string is a huge natural number that represents a function. Thus if you can find the Gödelized function, then all functions are computable by both formalisms. I find this a bit distasteful - when we compute with CPUs we don't actually compute Gödel numbers!
This is not correct. The concept of algorithm has nothing intrinsic to do with natural numbers. You could use any data structure, e.g. finite strings of symbols from a fixed (per application) finite alphabet as is used in Post normal systems. The Lambda Calculus is also an example, as it doesn't use natural numbers, but its own expressions.
The class of computations that Church and Turing are equivalent are the functions from N to N (encoding required obvs), as proven by Turing. Everything else is conjecture.
Turing gives "computable by Turing machine", and Church gives "effectively calculable by the lambda calculus". Kleene holds them both to be the same, culminating in Theorem XXX. This misses a subtle point that this only applies up to the class of functions from N->N.
When the class of functions is S->S, where S is a string or tree of symbols, lambda calculus runs into some minor issues. For example, you cannot define equality of terms in lambda calculus nor can lambda calculus realize itself.
Bob Harper's book is the only book I know of that was explicit about this fact, though he dismisses it as a minor issue. Barendregt surprisingly also missed this.
I'd be careful with that, you need to formalize "any possible algorithm" first, and that's the content of Church-Turing I believe.
Edit: Also, don't forget recursive functions (dating from I don't know when, actually)
To my knowledge, recursive functions alone are not sufficient to describe all computation. To do that, you need to consider functions as first-class values which is the innovation Alonzo Church came up with concurrently with Turing’s work.
> recursive functions alone are not sufficient to describe all computation.
Any function computable with TM is recursive, and vice versa, so they should be, if you understand "computable" as "computable with a TM". I don't see how this "functions as first class" comes into play here, but I'd be interested anyway?
Before Church, functions weren’t considered mathematical objects that could be passed as arguments to another function, for instance. I don’t recall the details, but this allows some computations that can’t be described by recursion of fixed functions.
This strikes me as profoundly ahistorical. Mathematicians have considered function spaces as families of objects to be operated upon by higher-order functions (themselves considered objects to be operated on, and so on) long before the 1930s. I'm sure some version of this thinking has been part of the "folklore" of mathematics for centuries, but at the very least you have to recognize that the idea of higher-order functions is subsumed by Cantorian set theory in the 19th century.
Edit: if you mean to say that a formalism for higher-order functions was novel in its presence in a computational calculus, your remark makes a little more sense. But a few remarks on that:
* Already in 1933, Herbrand–Gödel μ-recursion had given a model of computation that was equivalent to the lambda calculus. (This could be the "recursion" that the post you're responding to was referencing.) I guess the μ operator could be regarded as a higher-order function, but functions don't really play a first-class role in the μ-calculus.
* It's probably more accurate to say that the lambda calculus was conceived as a logical formalism, of which Church published only a computational fragment when it became apparent that the original calculus was afflicted with the Kleene-Rosser paradox. Higher-order functions (and predicates) had already played a role in formal logic systems for decades prior to this.