Skip to main content
added 384 characters in body
Source Link

Edit I have read Fedor Pakhomov's comment above and his comment contains all points essential in my answer but in a much compressed form. Indeed, substitutions may be seen as forming a DAG, and Fedor also uses an argument from the rate of growth of iterated squaring vs. the linear length of a term in a DAG-like form. So my answer is rather an elaboration on Fedor's comment. End of edit

Let me provide an example of such a non-regular coding which I believe is not completely ``out of the blue''. The inspiration for it comes from boolean circuits. There, a circuit is called a formula if all its internal nodes have out-degree at most one. This means that we cannot use a function computed by a node more than once. Such a circuit easily translates into a boolean formula of a similar size. I'll do the opposite.

Imagine that while making our Gödel coding we want to be space efficient. So, while computing $\xi(t)$, we want to code efficiently subterms which appear more than once in a term $t$. This corresponds to a situation when we allow arbitrary circuits to code our terms and formulas.

Assume that we want to code a term $t$ which is of the form $t'(s\backslash x)$, where $x$ occurs in $t'$ more than once and $x$ does not occur in $t$. Then, we may represent $t$ as a sequence $(s \rightarrow x)(t')$. Of course, while writing down $t'$ and $s$ we use the same trick recursively. Finally, the obtained sequence of symbols can be coded by any efficient coding of sequences of bits. Let $\xi$ be such a coding. The point is that such a method may decrease the length (and the size) of codes for terms with lots of regularities.

A coding as above is not regular. Let me provide an example. I take a sequence of terms. The term $t_0=2$ and $t_{i+1}=(t_i*t_i)$. The length of the term $t_i$ is $O(2^{i})$ and its the value is $2^{2^{i}}$. On the other hand, the length of a sequence describing $t_i$ with substitutions is $O(i\log_2(i))$ (the $\log_2(i)$ factor comes from the lengths of new variables in the sequence of substitutions). Such a sequence may look like this: $$ (2\rightarrow x_0)(x_0 * x_0\rightarrow x_1)(x_1*x_1\rightarrow x_2)\dots (x_{i-2}*x_{i-2}\rightarrow x_{i-1})(x_{i-1}*x_{i-1}). $$ As the length of this sequence is $O(i\log_2(i))$, the Gödel number for this sequence, $\xi(t_i)$, is of order $2^{O(i\log_2(i))}$.

Let $\text{val}(t)$ be the value of a term $t$. Now, let us assume that $2<\xi(2)$ and let us take $i$ big enough. I claim that it is impossible that $\forall j<i (\xi(t_j)*\xi(t_j)< \xi(t_{j+1}))$. It this would be the case, then for all $j\leq i$ the value of $t_j$ would be less then $\xi(t_j)$. But this is impossible, as the value of $t_i$ is $2^{O(2^i)}$ while $\xi(t_i)$ is $2^{O(i\log_2(i))}$.

PS. The above coding allows to reconstruct $t$ from $\xi(t)$. But $\xi(t)$ depends on the choice of terms $s$ that we substitute. If one would like to make $\xi(t)$ unique, then one should fix this choice. E.g. one could always choose the longest term $s$ which occurs more than once in $t$ and the leftmost one if such $s$ is not unique.

PPS. If we have totality of $\exp$ then the function computing a value of a term from its code is total. However, in models of weak arithmetics (without $\exp$) we may have codes of terms for which ''values'' would be "outside" a model.

Let me provide an example of such a non-regular coding which I believe is not completely ``out of the blue''. The inspiration for it comes from boolean circuits. There, a circuit is called a formula if all its internal nodes have out-degree at most one. This means that we cannot use a function computed by a node more than once. Such a circuit easily translates into a boolean formula of a similar size. I'll do the opposite.

Imagine that while making our Gödel coding we want to be space efficient. So, while computing $\xi(t)$, we want to code efficiently subterms which appear more than once in a term $t$. This corresponds to a situation when we allow arbitrary circuits to code our terms and formulas.

Assume that we want to code a term $t$ which is of the form $t'(s\backslash x)$, where $x$ occurs in $t'$ more than once and $x$ does not occur in $t$. Then, we may represent $t$ as a sequence $(s \rightarrow x)(t')$. Of course, while writing down $t'$ and $s$ we use the same trick recursively. Finally, the obtained sequence of symbols can be coded by any efficient coding of sequences of bits. Let $\xi$ be such a coding. The point is that such a method may decrease the length (and the size) of codes for terms with lots of regularities.

A coding as above is not regular. Let me provide an example. I take a sequence of terms. The term $t_0=2$ and $t_{i+1}=(t_i*t_i)$. The length of the term $t_i$ is $O(2^{i})$ and its the value is $2^{2^{i}}$. On the other hand, the length of a sequence describing $t_i$ with substitutions is $O(i\log_2(i))$ (the $\log_2(i)$ factor comes from the lengths of new variables in the sequence of substitutions). Such a sequence may look like this: $$ (2\rightarrow x_0)(x_0 * x_0\rightarrow x_1)(x_1*x_1\rightarrow x_2)\dots (x_{i-2}*x_{i-2}\rightarrow x_{i-1})(x_{i-1}*x_{i-1}). $$ As the length of this sequence is $O(i\log_2(i))$, the Gödel number for this sequence, $\xi(t_i)$, is of order $2^{O(i\log_2(i))}$.

Let $\text{val}(t)$ be the value of a term $t$. Now, let us assume that $2<\xi(2)$ and let us take $i$ big enough. I claim that it is impossible that $\forall j<i (\xi(t_j)*\xi(t_j)< \xi(t_{j+1}))$. It this would be the case, then for all $j\leq i$ the value of $t_j$ would be less then $\xi(t_j)$. But this is impossible, as the value of $t_i$ is $2^{O(2^i)}$ while $\xi(t_i)$ is $2^{O(i\log_2(i))}$.

PS. The above coding allows to reconstruct $t$ from $\xi(t)$. But $\xi(t)$ depends on the choice of terms $s$ that we substitute. If one would like to make $\xi(t)$ unique, then one should fix this choice. E.g. one could always choose the longest term $s$ which occurs more than once in $t$ and the leftmost one if such $s$ is not unique.

PPS. If we have totality of $\exp$ then the function computing a value of a term from its code is total. However, in models of weak arithmetics (without $\exp$) we may have codes of terms for which ''values'' would be "outside" a model.

Edit I have read Fedor Pakhomov's comment above and his comment contains all points essential in my answer but in a much compressed form. Indeed, substitutions may be seen as forming a DAG, and Fedor also uses an argument from the rate of growth of iterated squaring vs. the linear length of a term in a DAG-like form. So my answer is rather an elaboration on Fedor's comment. End of edit

Let me provide an example of such a non-regular coding which I believe is not completely ``out of the blue''. The inspiration for it comes from boolean circuits. There, a circuit is called a formula if all its internal nodes have out-degree at most one. This means that we cannot use a function computed by a node more than once. Such a circuit easily translates into a boolean formula of a similar size. I'll do the opposite.

Imagine that while making our Gödel coding we want to be space efficient. So, while computing $\xi(t)$, we want to code efficiently subterms which appear more than once in a term $t$. This corresponds to a situation when we allow arbitrary circuits to code our terms and formulas.

Assume that we want to code a term $t$ which is of the form $t'(s\backslash x)$, where $x$ occurs in $t'$ more than once and $x$ does not occur in $t$. Then, we may represent $t$ as a sequence $(s \rightarrow x)(t')$. Of course, while writing down $t'$ and $s$ we use the same trick recursively. Finally, the obtained sequence of symbols can be coded by any efficient coding of sequences of bits. Let $\xi$ be such a coding. The point is that such a method may decrease the length (and the size) of codes for terms with lots of regularities.

A coding as above is not regular. Let me provide an example. I take a sequence of terms. The term $t_0=2$ and $t_{i+1}=(t_i*t_i)$. The length of the term $t_i$ is $O(2^{i})$ and its the value is $2^{2^{i}}$. On the other hand, the length of a sequence describing $t_i$ with substitutions is $O(i\log_2(i))$ (the $\log_2(i)$ factor comes from the lengths of new variables in the sequence of substitutions). Such a sequence may look like this: $$ (2\rightarrow x_0)(x_0 * x_0\rightarrow x_1)(x_1*x_1\rightarrow x_2)\dots (x_{i-2}*x_{i-2}\rightarrow x_{i-1})(x_{i-1}*x_{i-1}). $$ As the length of this sequence is $O(i\log_2(i))$, the Gödel number for this sequence, $\xi(t_i)$, is of order $2^{O(i\log_2(i))}$.

Let $\text{val}(t)$ be the value of a term $t$. Now, let us assume that $2<\xi(2)$ and let us take $i$ big enough. I claim that it is impossible that $\forall j<i (\xi(t_j)*\xi(t_j)< \xi(t_{j+1}))$. It this would be the case, then for all $j\leq i$ the value of $t_j$ would be less then $\xi(t_j)$. But this is impossible, as the value of $t_i$ is $2^{O(2^i)}$ while $\xi(t_i)$ is $2^{O(i\log_2(i))}$.

PS. The above coding allows to reconstruct $t$ from $\xi(t)$. But $\xi(t)$ depends on the choice of terms $s$ that we substitute. If one would like to make $\xi(t)$ unique, then one should fix this choice. E.g. one could always choose the longest term $s$ which occurs more than once in $t$ and the leftmost one if such $s$ is not unique.

PPS. If we have totality of $\exp$ then the function computing a value of a term from its code is total. However, in models of weak arithmetics (without $\exp$) we may have codes of terms for which ''values'' would be "outside" a model.

Source Link

Let me provide an example of such a non-regular coding which I believe is not completely ``out of the blue''. The inspiration for it comes from boolean circuits. There, a circuit is called a formula if all its internal nodes have out-degree at most one. This means that we cannot use a function computed by a node more than once. Such a circuit easily translates into a boolean formula of a similar size. I'll do the opposite.

Imagine that while making our Gödel coding we want to be space efficient. So, while computing $\xi(t)$, we want to code efficiently subterms which appear more than once in a term $t$. This corresponds to a situation when we allow arbitrary circuits to code our terms and formulas.

Assume that we want to code a term $t$ which is of the form $t'(s\backslash x)$, where $x$ occurs in $t'$ more than once and $x$ does not occur in $t$. Then, we may represent $t$ as a sequence $(s \rightarrow x)(t')$. Of course, while writing down $t'$ and $s$ we use the same trick recursively. Finally, the obtained sequence of symbols can be coded by any efficient coding of sequences of bits. Let $\xi$ be such a coding. The point is that such a method may decrease the length (and the size) of codes for terms with lots of regularities.

A coding as above is not regular. Let me provide an example. I take a sequence of terms. The term $t_0=2$ and $t_{i+1}=(t_i*t_i)$. The length of the term $t_i$ is $O(2^{i})$ and its the value is $2^{2^{i}}$. On the other hand, the length of a sequence describing $t_i$ with substitutions is $O(i\log_2(i))$ (the $\log_2(i)$ factor comes from the lengths of new variables in the sequence of substitutions). Such a sequence may look like this: $$ (2\rightarrow x_0)(x_0 * x_0\rightarrow x_1)(x_1*x_1\rightarrow x_2)\dots (x_{i-2}*x_{i-2}\rightarrow x_{i-1})(x_{i-1}*x_{i-1}). $$ As the length of this sequence is $O(i\log_2(i))$, the Gödel number for this sequence, $\xi(t_i)$, is of order $2^{O(i\log_2(i))}$.

Let $\text{val}(t)$ be the value of a term $t$. Now, let us assume that $2<\xi(2)$ and let us take $i$ big enough. I claim that it is impossible that $\forall j<i (\xi(t_j)*\xi(t_j)< \xi(t_{j+1}))$. It this would be the case, then for all $j\leq i$ the value of $t_j$ would be less then $\xi(t_j)$. But this is impossible, as the value of $t_i$ is $2^{O(2^i)}$ while $\xi(t_i)$ is $2^{O(i\log_2(i))}$.

PS. The above coding allows to reconstruct $t$ from $\xi(t)$. But $\xi(t)$ depends on the choice of terms $s$ that we substitute. If one would like to make $\xi(t)$ unique, then one should fix this choice. E.g. one could always choose the longest term $s$ which occurs more than once in $t$ and the leftmost one if such $s$ is not unique.

PPS. If we have totality of $\exp$ then the function computing a value of a term from its code is total. However, in models of weak arithmetics (without $\exp$) we may have codes of terms for which ''values'' would be "outside" a model.