Как комбинаторы с фиксированной запятой рекурсивные конструкции заканчиваются?

Question

Fixed-point combinators предоставляют возможность анонимным функциям ссылаться на себя или создавать взаимно рекурсивные структуры. Хотя они полезны в лямбда-исчислении, они по существу являются излишними в современных языках программирования, потому что большинство, если не все, поддерживают рекурсию, лямбды и замыкания.

Кроме того, комбинаторы с фиксированной запятой могут создавать рекурсивные конструкции, такие как леворекурсивные грамматические синтаксические анализаторы. Рассмотрим Lickman 1995, который доказывает прекращение его реализации, но на самом деле не упоминает , как работает (это просто поэтапный вывод из теории решетки в реализацию haskell) и , почему ему нужны компиляторы с фиксированной запятой на языке, который уже поддерживает рекурсию изначально.

Как это работает и почему ему нужен комбинатор с фиксированной запятой?

Answer 1

Из быстрого сканирования, в конце 5.3, Ликман пишет: «Как определено выше, fixS обеспечивает достаточную производительность на всех непрерывных входах».

Задача состоит в том, чтобы заставить оператор фиксированной точки производить достаточный вывод, чтобы синтаксический анализ продолжался. Вы не можете сделать это для общего fix :: (a -> a) -> a, но специализируясь на a до Set a или позже Parser a, дает достаточно структуры (а именно решетки) для работы.

Опять же, я только что просмотрел тезис, но я считаю, что доказательство (в разделе 5.5) утверждения «h :: Parser a -> Parser a поддерживает свойство производительности ==>fixP h является продуктивным» является ключевым.

Answer 2

Обязательно. Вот простой правой рекурсивной грамматики трех правил:

S -> b T 
T -> a S 
T -> a 

Эти три правила позволяют нам построить синтаксический анализатор для распознавания этих строк:

type Parser = String -> (Bool, String) 
s :: Parser 
s "" = (False, "") 
s (c : cs) = if c == 'b' then t cs else (False, cs) 

t :: Parser 
t "" = (False, "") 
t (c : cs) 
    | c == 'a' && cs == "" = (True, "") 
    | c /= 'a' = (False, cs) 
    | otherwise = s cs 

Если вы хотите сделать более общий синтаксический анализ, просто специализируются Bool, чтобы вместо этого иметь некоторую структуру данных, возможно, сохраненную в файле Maybe, чтобы указать отказ. Возврат (False, ___) при неудачном анализе помог бы, если бы у S были и другие правила, например, например. S -> T T и T -> b b. Затем, когда мы получаем «b», за которым следует (False, ___), мы перемотаем, чтобы попробовать S -> T T. Такого рода грамматики можно сделать с небольшим количеством жира и рекурсии локтя.

Три правила, описанные выше, будут успешно соответствовать строкам типа «ба», «баба» и т. Д. Мы также могли бы написать эти строки слева рекурсивно:

S -> T a 
T -> S b 
T -> b 

Что произойдет, если вы пытаетесь писать одни и те же парсер выше? Бесконечный цикл, если вы смотрите на фронт строки. Проблема в том, что функция S сначала вызовет функцию T, а затем T сначала вызовет S, и они будут взаимно рекурсивно считать бесконечность. Компьютер не настолько умен, чтобы знать, что постусловия («за которым следует а», «за которым следует а») делает невозможным дальнейшее решение; он просто спускается в ваши функции и надеется, что вы знаете, что делаете.

Как хорошо сочетается комбинатор с фиксированной запятой? Ну, подумайте об этих правилах как о описании дерева: тогда оценка функции пересекает эту глубину дерева, и это конкретное дерево бесконечно в этом направлении.С другой стороны, обход по ширине может основываться на этих правилах и может поднять результат, который использует наименьшую из этих функций, и это «наименее фиксированная точка» для определенной функции, основанной на этой грамматике. Таким образом, поэтому правый комбинатор с фиксированной запятой (основанный либо на diag в статье, либо на комбинаторе теории решетки) может прекратиться при описании этих правил, тогда как наивная рекурсия не будет.