algorithm - 是否有快速算法来确定上下文无关语言术语的哥德尔数？

Question

假设我们有一个简单的语法规范。有一种方法可以枚举该语法的术语，保证任何有限术语都具有有限位置，by iterating it diagonally .例如，对于以下语法:

S      ::= add
add    ::= mul | add + mul
mul    ::= term | mul * term
term   ::= number | ( S )
number ::= digit | digit number
digit  ::= 0 | 1 | ... | 9

您可以像这样枚举术语:

0
1
0+0
0*0
0+1
(0)
1+0
0*1
0+0*0
00
... etc

我的问题是:是否有相反的方法？也就是说，采用该语法的有效术语，例如 0+0*0，并找到它在此类枚举中的位置 - 在这种情况下，9?

Answer 1

对于这个特定的问题，如果我们允许自己选择不同的枚举顺序，我们可以设计出一些相当简单的东西。这个想法基本上是Every Bit Counts中的那个。 ，我也在评论中提到了这一点。首先，一些准备工作:一些导入/扩展、表示语法的数据类型和 pretty-print 。为简单起见，我的数字最多为 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 列表。好的!让我们开始吧。我们将为 Godel-able 事物定义一个类，这些事物可以在数字之间来回转换——索引到居民的无限列表中。稍后我们将检查此翻译是否与我们在上面定义的枚举匹配。

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

此处对的实例是标准康托尔对角线。这只是一点代数:使用三角形数字计算出你要去哪里/来自哪里。现在为这个类构建实例是一件轻而易举的事。 Number 仅以 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)

就是这样!我们现在可以“有效地”在语法分析树和它们的 Godel 编号之间来回转换这个语法。此外，这个翻译符合上面的列举，你可以验证:

*Main> map from [0..29] == take 30 ss
True

我们确实滥用了这个特定语法的许多很好的特性——非歧义性，事实上几乎所有的非终结符都有无限多的派生——但是这种技术的变化可以让你走得很远，特别是如果你不是太严格的话要求每个数字都与独特的东西相关联。

此外，顺便说一句，您可能会注意到，除了 (Nat, Nat) 的实异常(exception)，这些 Godel 编号特别好，因为它们查看/产生一个位(或 trit ) 一次。所以你可以想象做一些流媒体。但是 (Nat, Nat) 非常讨厌:您必须提前知道整数才能计算 sqrt。实际上，您也可以将它变成一个流媒体播放器，而不会失去密集的特性(每个 Nat 都与一个唯一的 (Nat, Nat) 相关联)，但那是一个topic for another answer ...