-3
$\begingroup$

We see here the following statement about Godelization:

Gödel numbering in computer science means more or less "source code" and "data in binary format", so I hope the significance of this should be obvious if I can convince you that this really is so.

Before modern computers came into existence, people made single-purpose computing devices (I am telling you a story, not a history), for example someone made a machine for calculating arctanarctan, and someone else made a machine for calculating the Bessel function. Turing's original insight was that we only had to build one machine (the universal one), which took as input the description of any machine and simulated it. But what is a "description of a machine"? An engineer might think of circuit designs and assembly instructions. But that is very complicated and not easily presented to a machine. And perhaps ever more complicated machines require ever more complicated descriptions?

We need a way of describing machines that is as simple as possible. Here Gödel's idea was important: he showed some years before Turing that all sorts of things in logic (formulas, proofs) could be encoded with numbers, and then manipulated within arithmetic. We can do a similar trick with Turing machines: encode the program, the current state, and the contents of the tape used so far, with a string of symbols on a tape (for examples 00's and 11's), and then manipulate the string with a Turing machine.

We see here the following explanation of Church-encoding:

In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The data and operators form a mathematical structure which is embedded in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.

Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding. The Church-Turing thesis asserts that any computable operator (and its operands) can be represented under Church encoding. In the untyped lambda calculus the only primitive data type is the function.

This statement appears to combine to two in a way that says they're orthogonal (ie that being church-encoded or not is irrelevant to the Gödelization process) - but I'm not sure:

So let's say that you have natural numbers (or a Church encoding of natural numbers) in your typed lambda calculus. It's possible to do a Gödel numbering that assigns every term in System F to a unique natural number.

My question is: Can we say that Church encoding is a form of Gödelization?

$\endgroup$
  • 1
    $\begingroup$ Is there a scientific question here? It seems awfully vague to ask this question. For instance, why would "Yes we can" be an insufficient answer? $\endgroup$ – Andrej Bauer Apr 2 '16 at 8:57
  • $\begingroup$ Perhaps with an illustration of why you can and a pointer to further reading. Some reasoning would be good too. Perhaps even pointing out flaws in the authors understanding might help. $\endgroup$ – hawkeye Apr 2 '16 at 9:35
  • $\begingroup$ Well, in that case this question should be asked at cs.stackexchange.com. There's nothing research-level about it. $\endgroup$ – Andrej Bauer Apr 2 '16 at 19:17
1
$\begingroup$

It's possible to do a Gödel numbering that assigns every term in System F to a unique natural number?

The answer is yes, pick your favorite way of coding terms in F, simply because they are countable number of expressions.

Just being able to assign numbers to expressions in a system is not useful by itself, the question is can it be done in a manner that supports some operations, e.g. substitution, inside the system. The answer is again yes, the standard one works, operations are computable in Girard's F.

Can we say that Church encoding is a form of Gödelization?

Church encoding is an encoding of natural numbers by lambda terms, it is not an arithmetization of a language (the correct terminology is arithmetization not Godelization). For arithmetization of a language we need some way of representing natural numbers in a language, but that is independent of the arithmetization of the language itself.

But really the more important question is why would one want to arithmetize a language? Godel does it to be able to talk about the language itself in arithmetic and perform computation over the language. If you think about it what we really want is to talk about computation of functions over the syntactic expressions of a language, and we arithmetize because arithmetic can only talk about numbers. It is just a way of representing language expressions as numbers so we can talk about computation over them, the same way we encode language, numbers, graphs, etc. as binary strings when we deal with computers. Arithmetization was ingenious at the time of Godel, but now it is kind of trivial (in a sense) for a computer programmer. We can encode a formal language as numbers and perform computation over it, sure.

Finally, if you can arithmetize language in a system, you can arithmetize langauge in any system extending it. The syntactic constructions that one is interested do not change from say PA to Godel's T to Girard's F.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.