【问题标题】:Is there a fast algorithm to determine the godel number of a term of a context free language?是否有一种快速算法来确定上下文无关语言的术语的哥德尔数?
【发布时间】:2014-05-28 22:59:41
【问题描述】:

假设我们有一个简单的语法规范。有一种方法可以枚举该语法的术语,以保证任何有限术语都有一个有限位置,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?

【问题讨论】:

  • 枚举直到你遇到这个词?不过,这显然并不快。不过我会将此发布到 CS,但我认为 SO 不再适合这种事情了。
  • 我敢猜测 CS 也不是适合它的地方。我很难想象会有一种情况会关心哥德尔编号算法的效率。
  • 你要求枚举是“密集的”,没有间隙吗?使用结构递归对自然进行注入很容易,但双射似乎更难。
  • @rici- 我的错,你是对的.... 语法中内置了左结合性,我没有注意到这一点。我现在更强烈地认为我的第二条评论是正确的。当我考虑只使用number:= 0|1, sum := number | sum + number 的更简单的情况时,看起来位置是(类似于)2^(#sum)+b,其中#sum=<count of "+"s>b=<binary number formed by the terminals in order>。不过,我仍然不想把我的大脑包裹在完整的问题上,我很高兴自己说服自己这可能是正确的答案。 :)
  • 这正是序列化库解决的问题:我们如何将给定的 ADT(您可以将其视为语法)紧凑地表示为位,并从这些位中有效地恢复 ADT?通常,我们不期望每个位串对应某个值;这使问题变得更加困难。但您可能对Every Bit Counts 的论文感兴趣。

标签: algorithm haskell grammar context-free-grammar


【解决方案1】:

对于这个特定的问题,如果我们允许自己选择不同的枚举顺序,我们可以做一些相当简单的事情。这个想法基本上是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

好的,现在让我们开始吧。假设我们有两个无限列表ab。有两点需要注意。首先,在a +++ b 中,所有偶数索引都来自a,所有奇数索引都来自b。所以我们可以查看索引的最后一位来查看要查看的列表,剩余的位来选择该列表中的索引。其次,在a +*+ b 中,我们可以使用数字对和单个数字之间的标准双射来转换大列表中的索引和ab 列表中的索引对。好的!让我们开始吧。我们将为可以在数字之间来回转换的可哥德尔事物定义一个类——索引到无限的居民列表中。稍后我们将检查此翻译是否与我们在上面定义的枚举匹配。

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...

【讨论】:

  • 我希望你从我的问题中得到的所有业力都足以支付你教给我的一切,否则我会欠下一笔巨款。
  • @Viclib 我很高兴你正在学习!这对我来说已经足够回报了。
猜你喜欢
  • 2015-04-25
  • 2011-03-31
  • 1970-01-01
  • 1970-01-01
  • 2012-12-18
  • 1970-01-01
  • 1970-01-01
  • 2012-03-15
  • 1970-01-01
相关资源
最近更新 更多