是否有快速算法来确定上下文无关语言的godel数？

Question

假设我们有一个简单的语法规范.有一种方法可以枚举该语法的术语,通过对角迭代来保证任何有限项都具有有限的位置.例如,对于以下语法:

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中的一个,我在评论中也提到过.首先,一些预备知识:一些导入/扩展,一个表示语法的数据类型,以及一个漂亮的打印机.为了简单起见,我的数字最多只能达到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文档中有关这些的更多信息.我们将保留的一个不变量是我们的列表 - 除了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能够定义一个类 - 指向无限的居民列表.稍后我们将检查此转换是否与我们上面定义的枚举相匹配.

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

这里对的实例是标准的Cantor对角线.这只是一些代数:使用三角形数字来确定你的去向/来自哪里.现在为这个类构建实例是一件轻而易举的事.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)

就是这样!我们现在可以"有效地"在解析树和它们的Godel编号之间来回翻译这个语法.此外,此转换符合上述枚举,您可以验证:

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

我们确实滥用了这种特殊语法的许多不错的属性 - 非歧义,事实上几乎所有的非终结者都有无限多的推导 - 但这种技术的变化可以让你走得很远,特别是如果你不是太严格要求每一个数字与唯一的东西相关联.

顺便说一下,你可能会注意到,除了实例之外(Nat, Nat),这些Godel编号特别好看,因为它们一次查看/生成一个位(或trit).所以你可以想象做一些流媒体.但是这个(Nat, Nat)非常讨厌:你必须提前知道整数才能计算出来sqrt.你实际上可以把它变成一个流媒体人,而不会失去密集的属性(每个Nat都与一个独特的相关(Nat, Nat)),但这是另一个答案的话题 ......