Является ли моя грамматика исчисления лямбда однозначной?

Question

Я пытаюсь написать небольшой компилятор для языка, который обрабатывает лямбда-исчисление. Вот неоднозначное определение языка, что я нашел:.

E →^v . E | E E | (E) | v 

Символы ^,, (,) и v являются лексемы.^представляет лямбда, а v представляет собой переменную. Выражение вида^v.E является определением функции, где v - формальный параметр функции, а E - его тело. Если f и g - лямбда-выражения, то лямбда-выражение fg представляет собой применение функции f к аргументу g.

Я пытаюсь написать однозначную грамматику для этого языка в предположении, что функциональное приложение оставлено ассоциативным, например, fgh = (fg) h, и эта функция приложения связывается более жестко, чем., Например, (^ x ..^у й)^ZZ = (..^х (^ у й))^ZZ

Вот то, что я до сих пор, но я не уверен, если это правильно:

E -> ^v.E | T 
T -> vF | (E) E 
F -> v | epsilon 

Может ли кто-нибудь помочь?

Answer 1

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

Лучшая книга, которую я имею, а это не значит, что самая лучшая книга - Types and Programming Languages (WorldCat) от Benjamin C. Pierce. Я знаю, что название звучит не как лямбда-исчисление, а взгляните на λ-Calculus extensions: meaning of extension symbols, в котором перечислены многие из лямбда-исчислений, которые исходят из книги. Есть код для книги: OCaml и F#.

Попробуйте найти в CiteSeerX для исследований по исчислению лямбда, чтобы узнать больше.

Лучший λ-исчисление оценщик я нашел до сих пор:

Lambda calculus reduction workbench с информацией here.

Кроме того, я нахожу, что вы получите гораздо лучшие ответы на вопросы лямбда-исчисления, связанные с программированием, на CS:StackExchange и связанные с математикой вопросы в Math:StackExcahnge.

Что касается языков программирования для реализации лямбда-исчисления, вам, вероятно, потребуется узнать functional language, если вы этого не сделали; Да, это другой зверь, но просветление на другой стороне горы впечатляет. Большая часть исходного кода, который я нахожу, использует функциональный язык, такой как ML или OCaml, и как только вы его изучаете, остальным становится легче учиться.

Чтобы быть более конкретным, here исходным код для бестипового исчисления проекта лямбды, here является входным файлом на F # варьирование YACC, который от чтения вашего предыдущего questions, кажется, в вашем мире знаний и here является образец ввод.

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

Наконец мы добираемся до части вы после

Примечания LCID является идентификатором нижнего регистра

Term : AppTerm 
    | LAMBDA LCID DOT Term 
    | LAMBDA USCORE DOT Term 

AppTerm : ATerm 
     | AppTerm ATerm 

/* Atomic terms are ones that never require extra parentheses */ 
ATerm : LPAREN Term RPAREN 
     | LCID 

Answer 2

Вы можете найти доказательство двусмысленности конкретной грамматики в сублинейное время, но доказать, что грамматика однозначно является NP полной проблемой. Вам нужно будет генерировать все возможные предложения на этом языке и проверить, что для каждого из них есть только один вывод.