diff options
| -rw-r--r-- | sec/systemt.ltx | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index 7ed5870..c9f280b 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -151,19 +151,19 @@ is lacking in some regard. \subsubsection*{G\"odel Encodings} -G\"odel encodings represent inductive data types as natural -numbers. It is well-known that there are pairing functions, bijections -from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use -these functions to encode inductive types as pairs of tags and -payloads, such that every constructor has a unique tag. Writing -\(\tuple{\cdot, \cdot}\) for a chosen pairing function, we can encode the -binary tree constructors as +G\"odel encodings~\cite{dialectica?} represent data types as natural +numbers. It is well-known that there are pairing functions, invertible +functions from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive +recursive~\cite{pairing}. We can use pairing functions to encode +inductive types as pairs of tags and payloads, such that every +constructor has a unique tag. Writing \(\tuple{\cdot, \cdot}\) for a chosen +pairing function, we can encode the binary tree constructors as \begin{align*} \mathsf{leaf}(n) &\coloneq \tuple{0, n} \\ \mathsf{branch}(l, r) &\coloneq \tuple{1, \tuple{l, r}}. \end{align*} -One can pattern match on G\"odel encodings by using the unpairing part of -the bijection to split a value back into the tag and payload. +One can pattern match on G\"odel encodings by unpairing a value to +split it back into the tag and payload. One major limitation of G\"odel encodings is that they cannot represent higher-order data such as functions. The defining trait of |