Parsing challenge: Notacja dot. Starego logika

Question

W "Bustley Rosser's" Logic for Mathematicians "używa notacji, aby uniknąć zbyt wielu nawiasów. Chociaż nie wiem, kiedy logicy zaczynają używać tej notacji, ale wiem, że książka ta została opublikowana po raz pierwszy w 1957 roku, a także J. G. P. Nicod's paper, która została opublikowana w 1916 roku, również używa tej notacji. Jest więc oczywiste, że ma dość długą historię, choć obecnie nie jest to preferowane przez współczesnych logików.

W świecie programowania, w językach programowania LISP istnieje duże wyzwanie dla programistów, aby śledzić właściwą (ogromną!) Liczbę nawiasów. Haskell zapewnia operatorowi $, który zapewnia część funkcjonalności, ale ponieważ nie można powiedzieć, że jest to 2 * $ 3 + 4, nie jest tak potężny jak kropki (patrz przykłady poniżej). Seriale w języku C używają konwencjonalnego priorytetu operacji, ale w niektórych przypadkach nadal wymagane są nawiasy zagnieżdżone. Zastanawiam się, dlaczego żadne rzeczywiste języki nie używają tej strategii? Próbowałem, ale nie znalazłem nawet gramatyki!

Pozwól mi pokazać przykładowy język kalkulatora zabawek z tylko dwoma operatorami + i *, a wszystkie terminy są liczbami całkowitymi.

Przy tym zapisie translater przekazuje następujące przypadki testowe:

1 + 3 .* 2 
= (1 + 3) * 2 
1 *. 3 + 2 
= 1 * (3 + 2) 
1 *. 2 +. 2 
= (1 * 2) + 2 
2 *: 2 + 3 .* 4 
= 2 * ((2 + 3) * 4) 

cann't wyjaśnić wszystkie szczegół tej notacji, kosztuje prawie 5 stron w książce Rosser za. Ale w genaralnym (i krótkim) kropce . przed lub po operatorze reprezentuje "separator", aby odepchnąć dwie strony. Dwukropek : jest silniejszym separatorem, trzy kropki .: lub :. jest jeszcze silniejszy, ale mniejszy niż :: i tak dalej.

Zastanawiam się, jak możemy napisać gramatykę dla powyższego języka, a następnie przeanalizować? Również, chociaż ta notacja została przestarzała, okazało się, że jest ona bardzo czytelna dla programisty. Jakie są jego zalety i wady?

Answer 1

Notacja Dot została najgłośniej wykorzystana przez Russella i Whiteheada w Principia Mathematica (1910-1913), ale notacja została zapożyczona od Guiseppe Peano. Był również używany przez Alonzo Church, Willarda Van Ormana Quine'a i innych wpływowych logików (patrz this entry w Encyklopedii Filozofii Stanforda).

Przy odrobinie praktyki nie jest trudno odczytywać formuły w dot-notation, ale nie jest to tak eleganckie, jak się wydaje. Na początek, Russell i Whitehead jednak okazało się przydatne w użyciu nawiasów z operatorem negacji ~:

*3·01. p.q .=. ~(~p v ~q)

jak w powyższym przykładzie pokazują, plamka jest wykorzystywany zarówno jako operatora koniunkcji oraz wyrażania pierwszeństwo. W konsekwencji silniejsza koniunkcja może być zapisana jako : lub nawet :..

Wreszcie, w celu zmniejszenia bałaganu wizualnego (przypuszczam), Russell i Whitehead również stosują zależności pierwszeństwa, w których zestaw operatorów jest podzielony na trzy grupy pierwszeństwa, tak że kropki dla operatora o wyższym priorytecie dominują taka sama liczba kropek dla operatora o niższym priorytecie. Pomiędzy operatorami o równym pierwszeństwie, nie jest legalne, aby liczba kropek była równa, ale Russell i Whitehead również zdefiniowali niektórych potrójnych operatorów, takich jak p v q v r, aby móc uniknąć określenia nieistotnego pierwszeństwa. (Dokładne zasady analizowania takich wyrażeń nigdy nie zostały sformułowane formalnie, o ile wiem, ale definicje pojawiają się w PM.)

Powiedziawszy to wszystko, nietrudno jest parsować notację kropkową za pomocą wariantu algorytmu stoczniowego. Niestety, nie można go analizować za pomocą gramatyki bezkontekstowej, przez co jest mniej przydatny w gramatyce wygenerowanej za pomocą zautomatyzowanych narzędzi. Nawet parsery GLR są ograniczone do CFG. (Fakt, że notacja kropkowa nie jest wolna od kontekstu, można udowodnić za pomocą lematu pompowania, jest to bardziej interesujące ćwiczenie niż zwykłe aplikacje do pompowania lematu, przynajmniej imho.)

Jeśli zezwolisz na CFG nieskończoną liczbę symboli (kropek) i odpowiadającą im nieskończoną liczbę reguł, to całkiem proste jest napisanie gramatyki (lub, dokładniej, szablonu gramatycznego, ponieważ większość reguł jest sparametryzowana za pomocą liczby punktów). Tak więc teoretycznie można sparsować wyrażenie kropki przez pierwsze skanowanie, aby znaleźć maksymalną liczbę użytych kropek, a następnie wygenerować odpowiednią skończoną wiązkę CFG z szablonu. (Wynikowy wynik to LALR (1) pod warunkiem, że zdefiniujesz oddzielny terminal dla każdej sekwencji kropek). W praktyce można to zrobić, używając predykatów w CFG, aby utworzyć parser z generatorem parsera, który pozwala predykaty (na przykład ANTLR, ale osobiście użyłbym generatora oddolnego, aby uniknąć błądzenia z lewą rekursją eliminacji.)

Należy zauważyć, że notacja kropkowa ma swój własny wariant "zbędnych nawiasów okrągłych" ", ponieważ możesz, przynajmniej teoretycznie, użyć więcej punktów niż to konieczne. Kiedy bawiłem się z powyższym (teoretycznym, ale niezbyt użytecznym) algorytmem - automatycznie generującym CFG - łatwiej było mi wymagać minimalnej ilości punktów, ponieważ w przeciwnym razie stworzysz znacznie więcej reguł jednostek. Nie mogłem znaleźć odczytywanej maszynowo kopii PM do przetestowania, ale podczas wszystkich poszukiwań nigdy nie znalazłem wyrażeń, które nie byłyby minimalne. Nie wiem, czy było to wynikiem kompulsywnej czystości, czy pomysłu, że tylko wyroki minimalnej liczby punktów były legalne.

Answer 2

Oto interesująca aplikacja. Perl6 pozwala na rozszerzenie języka, dodanie nowych operatorów i określenie ich priorytetu względem istniejących operatorów. Poniższy przykładowy kod definiuje operatorów. Testy poniżej przebiegają pomyślnie.

use v6; 
use Test; 

sub infix:<*.> ($a, $b) is looser(&infix:<+>) { $a * $b } 
sub infix:<.*> ($a, $b) is looser(&infix:<+>) { $a * $b } 
sub infix:<*:> ($a, $b) is looser(&infix:<*.>) { $a * $b } 
sub infix:<:*> ($a, $b) is looser(&infix:<.*>) { $a * $b } 

sub infix:<+.> ($a, $b) is looser(&infix:<*.>) { $a + $b } 
sub infix:<.+> ($a, $b) is looser(&infix:<.*>) { $a + $b } 
sub infix:<+:> ($a, $b) is looser(&infix:<*:>) { $a + $b } 
sub infix:<:+> ($a, $b) is looser(&infix:<:*>) { $a + $b } 

# Tests 

is 1 + 3 .* 2, 
    (1 + 3) * 2; 

is 1 *. 3 + 2, 
    1 * (3 + 2); 

is 1 *. 2 +. 2, 
    (1 * 2) + 2; 

is 2 *: 2 + 3 .* 4, 
    2 * ((2 + 3) * 4);