diff options
| -rw-r--r-- | sec/systemt.ltx | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/sec/systemt.ltx b/sec/systemt.ltx index c9f280b..3abcdef 100644 --- a/sec/systemt.ltx +++ b/sec/systemt.ltx @@ -165,13 +165,12 @@ pairing function, we can encode the binary tree constructors as 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 -G\"odel encodings is that they represent data by natural numbers. As -function types cannot be encoded as naturals, we cannot encode -functions. We also cannot use a syntactic representation of functions; -\textcite{Squid:unpublished/Bauer17} proves there is no System~T term -that can recover a function from its syntax. +A major limitation of G\"odel encodings is that they cannot represent +higher-order data such as functions. G\"odel encodings by definition +encode data as natural numbers. We cannot encode arbitrary functions +as naturals, even in simple models such as \mathsf{Set}. If we +restrict ourselves to representable functions, \textcite{bauer} proves +we cannot recover a function from its syntax. Another difficulty with G\"odel encodings is implementing the fold operation. We require our chosen pairing function to be monotonic so |