假设我们有一个简单的语法规范。有一种枚举该语法项的方法,可以通过对角迭代来确保任何有限项都具有有限位置。例如,对于以下语法:
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?
0+0*0
对于这个特定的问题,如果我们允许自己选择不同的枚举顺序,那么我们可以做一些相当简单的事情。这个想法基本上是“ 每个位数”中的一个,我也在评论中提到了这一点。首先,进行一些初步准备:一些导入/扩展,代表语法的数据类型以及漂亮的打印机。为了简单起见,我的数字最多只能增加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始终是无限的。稍后这将很重要。
+++
+*+
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,我们可以使用数字对和单个数字之间的标准双射在大列表中的索引与aand中的索引对之间进行转换。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
这里的对的实例是标准的Cantor对角线。只是一些代数:使用三角形数字来确定您要去哪里/从哪里来。现在为此类创建实例很容易。Numbers以基数3表示:
Number
-- 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与unique关联(Nat, Nat)),但这是另一个答案的主题 …
(Nat, Nat)
sqrt
Nat