Существует ли быстрый алгоритм определения числа godel для термина контекстного свободного языка?

Ответ 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

Теперь определим порядок перечисления. Мы будем использовать два основных комбинатора, +++ для чередования двух списков (мнемонический: средний символ - это сумма, поэтому мы берем элементы из первого или второго) и +*+ для диагонализации (мнемоника: средний символ - это продукт, поэтому мы берем элементы как из первого, так и из второго аргументов). Подробнее об этом см. В документации . Один инвариант, который мы будем поддерживать, состоит в том, что наши списки - за исключением 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

Пример для пар здесь - стандартная диагональ Кантора. Это всего лишь немного алгебры: используйте числа треугольников, чтобы выяснить, откуда вы идете. Теперь создание экземпляров для этого класса - легкий ветерок. 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)

И это! Теперь мы можем "эффективно" переводить между деревьями синтаксического разбора и их нумерацией Геделя для этой грамматики. Более того, этот перевод соответствует приведенному выше перечислению, так как вы можете проверить:

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

Мы злоупотребляли многими хорошими свойствами этой конкретной грамматики - недвусмысленностью, тем фактом, что почти все нетерминалы имели бесконечное число выводов, но вариации по этой методике могут дать вам довольно далеко, особенно если вы не слишком строги требуя, чтобы каждое число было связано с чем-то уникальным.

Кроме того, вы можете заметить, что, за исключением экземпляра для (Nat, Nat), эти нумерации Геделя особенно хороши в том, что они смотрят/производят один бит (или трит) за раз. Таким образом, вы могли бы вообразить, как это происходит. Но (Nat, Nat) один довольно неприятный: вам нужно знать все число раньше времени, чтобы вычислить sqrt. Вы действительно можете превратить это в потокового парня тоже, не теряя свойство быть плотным (каждый Nat связан с уникальным (Nat, Nat)), но что тема для другого ответа...