[FOM] Short or very short Gôdel codes, anyone?

[Paul Tarau]

On Sat, Jul 14, 2012 at 9:25 PM, Richard Heck <richard_heck at brown.edu> wrote:
> On 07/12/2012 03:10 PM, Paul Tarau wrote:
>>
>> - only syntactically valid terms are encoded / decoded
>>
> Not to be overly picky, but mightn't one want the theory in question to
> prove, even to decide, such questions as: Is such-and-such well-formed?
>
> Richard
>

The encodings factor in obvious decidable properties of
our formal language objects (e.g well-formedness through an
unambiguous CF-grammar).

Term algebras can be seen as a generic syntax for well-formed
expressions in languages like predicate or lambda calculus as well
as a generic syntax for "proof-terms" in proof assistants like Coq.
Equivalently, they can be seen as programs expressed as syntax trees.

By restricting Goedel numberings to well formed terms
and ensuring that they are bijective, "no bit is lost"
through the mapping to natural numbers, e.g. optimal
information theoretical succinctness is achieved.

Paul Tarau