对于这个特定的问题,如果我们允许自己选择不同的枚举顺序,我们可以做一些相当简单的事情。这个想法基本上是Every Bit Counts中的那个,我在cmets中也提到过。首先,一些准备工作:一些导入/扩展、表示语法的数据类型和漂亮的打印机。为简单起见,我的数字只上升到 2(大到不再是二进制,但小到不会磨损我的手指和你的眼睛)。
{-# LANGUAGE TypeSynonymInstances #-}
import Control.Applicative
import Data.Universe.Helpers
type S = Add
data Add = Mul Mul | Add :+ Mul deriving (Eq, Ord, Show, Read)
data Mul = Term Term | Mul :* Term deriving (Eq, Ord, Show, Read)
data Term = Number Number | Parentheses S deriving (Eq, Ord, Show, Read)
data Number = Digit Digit | Digit ::: Number deriving (Eq, Ord, Show, Read)
data Digit = D0 | D1 | D2 deriving (Eq, Ord, Show, Read, Bounded, Enum)
class PP a where pp :: a -> String
instance PP Add where
pp (Mul m) = pp m
pp (a :+ m) = pp a ++ "+" ++ pp m
instance PP Mul where
pp (Term t) = pp t
pp (m :* t) = pp m ++ "*" ++ pp t
instance PP Term where
pp (Number n) = pp n
pp (Parentheses s) = "(" ++ pp s ++ ")"
instance PP Number where
pp (Digit d) = pp d
pp (d ::: n) = pp d ++ pp n
instance PP Digit where pp = show . fromEnum
现在让我们定义枚举顺序。我们将使用两个基本组合符,+++ 用于交错两个列表(助记符:中间字符是一个和,因此我们从第一个参数或第二个参数中获取元素)和 +*+ 用于对角化(助记符:中间的字符是一个产品,所以我们从第一个和第二个参数中获取元素)。有关这些的更多信息,请访问universe documentation。我们将保持的一个不变式是我们的列表——除了digits——总是无限的。这在以后很重要。
ss = adds
adds = (Mul <$> muls ) +++ (uncurry (:+) <$> adds +*+ muls)
muls = (Term <$> terms ) +++ (uncurry (:*) <$> muls +*+ terms)
terms = (Number <$> numbers) +++ (Parentheses <$> ss)
numbers = (Digit <$> digits) ++ interleave [[d ::: n | n <- numbers] | d <- digits]
digits = [D0, D1, D2]
让我们看几个术语:
*Main> mapM_ (putStrLn . pp) (take 15 ss)
0
0+0
0*0
0+0*0
(0)
0+0+0
0*(0)
0+(0)
1
0+0+0*0
0*0*0
0*0+0
(0+0)
0+0*(0)
0*1
好的,现在让我们开始吧。假设我们有两个无限列表a 和b。有两点需要注意。首先,在a +++ b 中,所有偶数索引都来自a,所有奇数索引都来自b。所以我们可以查看索引的最后一位来查看要查看的列表,剩余的位来选择该列表中的索引。其次,在a +*+ b 中,我们可以使用数字对和单个数字之间的标准双射来转换大列表中的索引和a 和b 列表中的索引对。好的!让我们开始吧。我们将为可以在数字之间来回转换的可哥德尔事物定义一个类——索引到无限的居民列表中。稍后我们将检查此翻译是否与我们在上面定义的枚举匹配。
type Nat = Integer -- bear with me here
class Godel a where
to :: a -> Nat
from :: Nat -> a
instance Godel Nat where to = id; from = id
instance (Godel a, Godel b) => Godel (a, b) where
to (m_, n_) = (m + n) * (m + n + 1) `quot` 2 + m where
m = to m_
n = to n_
from p = (from m, from n) where
isqrt = floor . sqrt . fromIntegral
base = (isqrt (1 + 8 * p) - 1) `quot` 2
triangle = base * (base + 1) `quot` 2
m = p - triangle
n = base - m
这里对的例子是标准的康托对角线。这只是一点代数:使用三角形数字来确定你要去/来自哪里。现在为这个类建立实例是一件轻而易举的事。 Numbers 仅以基数 3 表示:
-- this instance is a lie! there aren't infinitely many Digits
-- but we'll be careful about how we use it
instance Godel Digit where
to = fromIntegral . fromEnum
from = toEnum . fromIntegral
instance Godel Number where
to (Digit d) = to d
to (d ::: n) = 3 + to d + 3 * to n
from n
| n < 3 = Digit (from n)
| otherwise = let (q, r) = quotRem (n-3) 3 in from r ::: from q
对于剩下的三种类型,我们将按照上面的建议检查标记位以决定发出哪个构造函数,并将剩余的位用作对角化列表的索引。所有三个实例看起来都非常相似。
instance Godel Term where
to (Number n) = 2 * to n
to (Parentheses s) = 1 + 2 * to s
from n = case quotRem n 2 of
(q, 0) -> Number (from q)
(q, 1) -> Parentheses (from q)
instance Godel Mul where
to (Term t) = 2 * to t
to (m :* t) = 1 + 2 * to (m, t)
from n = case quotRem n 2 of
(q, 0) -> Term (from q)
(q, 1) -> uncurry (:*) (from q)
instance Godel Add where
to (Mul m) = 2 * to m
to (m :+ t) = 1 + 2 * to (m, t)
from n = case quotRem n 2 of
(q, 0) -> Mul (from q)
(q, 1) -> uncurry (:+) (from q)
就是这样!我们现在可以“有效地”在解析树和该语法的哥德尔编号之间来回转换。此外,此翻译与上述枚举匹配,您可以验证:
*Main> map from [0..29] == take 30 ss
True
我们确实滥用了这种特殊语法的许多好的特性——非歧义,几乎所有的非终结符都有无限多的派生——但这种技术的变化可以让你走得很远,特别是如果你不是太严格的话要求每个数字都与独特的事物相关联。
另外,顺便说一句,您可能会注意到,除了 (Nat, Nat) 的实例之外,这些 Godel 编号特别好,因为它们一次查看/产生一个位(或 trit)。所以你可以想象做一些流媒体。但是(Nat, Nat) 非常讨厌:你必须提前知道整数才能计算sqrt。你实际上也可以把它变成一个流媒体的家伙,而不会失去密集的属性(每个 Nat 都与一个唯一的 (Nat, Nat) 相关联),但那是一个 topic for another answer...