Dlaczego przepisywanie terminów?

12

Zrobiłem trochę googleingu i podszedłem trochę za krótko.

Zastanawiam się, jakie są główne powody dla naukowców zajmujących się obliczeniami, programistów, aby studiować przepisywanie terminów i / lub przepisywanie grafów terminowych.

O ile mogę stwierdzić, pomaga to w podstawowym rozumowaniu programów funkcjonalnych i (imperatywnej) kontroli programów. Najwyraźniej jest to temat bardzo interesujący dla logików i tych, którzy badają konstruktywne algebry abstrakcyjne.

Każda pomoc będzie mile widziana!

Musa Al-hassy
źródło

Odpowiedzi:

11

Nie jestem pewien, czy przyniesie ci to więcej niż już wiesz. Ale może nie rozumiem powodów, dla których zastanawiasz się nad przepisywaniem terminów. To pomaga.

Jak zapewne wiesz, gramatyki to systemy przepisywania ciągów. Na szczycie hierarchii Chomsky'ego znajdują się gramatyki typu 0, które definiują obliczenia rekurencyjnie policzalne (RE) i mają moc obliczeniową maszyn Turinga.

Oznacza to, że ogólnie systemy przepisywania mają wiele wspólnego z algorytmami wyrażania.

Problem z łańcuchami w ogóle polega na tym, że nie ma oczywistego sposobu na dołączenie do nich semantyki. Jest to rodzaj bezpostaciowego przepisywania.

To, co ludzie zazwyczaj są zainteresowani, to wyrażanie algorytmów w określonych domenach, które mają strukturę i właściwości. Domeny takie są często definiowane na podstawie elementarnych (atomowych) bytów i zamykane różnymi operacjami, być może ilorazowymi stosunkami równoważności i tak dalej. Są to często nazywane algebrami.

Domeny te są często abstrakcyjne. Ale obliczenia na ich elementach można wyrazić tylko na konkretnych reprezentacjach. Terminy są naturalną reprezentacją tych elementów, ponieważ wyrażają, w jaki sposób można uzyskać elementy dla innych elementów poprzez zastosowanie operacji, rekurencyjnie w dół do elementów atomowych (chociaż ogólne właściwości nie zawsze muszą iść w dół). Terminy są rodzajem składni struktury drzewa, którą można manipulować w celu wyrażenia algorytmów (tak jak w przypadku ciągu znaków). Ale struktura operandowa terminów pozwala również na powiązanie z nimi semantyki w jakiejś abstrakcyjnej dziedzinie za pomocą homomorfizmów.

Zamiast brać bardzo formalny pogląd na wikipedię i wiele tekstów na ten temat, wystarczy rozważyć programy. Zwykle uznaje się, że wygodną składnią reprezentacyjną programów jest tak zwane drzewo abstrakcyjnych składni (AST). Ale AST to tylko termin reprezentujący obiekt programu. Semantyka denotacyjna to sposób definiowania domen abstrakcyjnych i kojarzenia wartości z tych domen z AST (lub poddrzewami AST) za pomocą homomorfizmów. Programy w formie AST można przekształcić lub zoptymalizować, stosując reguły przepisywania (nie twierdzę, że wszystkie optymalizacje można lub należy wykonać w ten sposób).

Transformacja wyrażeń algebraicznych dla różnych celów może być wyrażona przez przepisywanie terminów. Na przykład uproszczenie niektórych wyrażeń. Różne typy obliczeń można również naturalnie wyrazić jako przepisywanie terminów, takie jak obliczanie pochodnych. Przepisywanie terminów jest również czasami używane do definiowania form kanonicznych w algebrach, gdy ta sama jednostka semantyczna może mieć kilka reprezentacji składniowych.

Radzę zajrzeć do artykułu w Wikipedii na ten temat .

Babou
źródło
6

Myślę, że to dlatego, że przepisywanie terminów jest czymś niezwykle podstawowym, a to pozwala opisywać rzeczy w bardzo niski sposób, niezależnie od jakiegokolwiek sprzętu.

Przepisywanie terminów może opisywać gramatykę, ale daje także mechanikę opisywanym systemom logicznym, takim jak logika pierwszego rzędu itp. Sprawdzanie i dedukcje można zapisywać jako zapisy terminów. Zatem zastąpienie przepisywania terminów jest tak naprawdę jedyną dostępną operacją. Prostota jest tutaj cenna, ponieważ opisujesz logikę, więc nie możesz wykorzystać pełnej złożoności logiki do opisania swojego systemu (ponieważ to jest system, który próbujesz opisać).

To daje ci mechanikę, której potrzebujesz, aby mówić o rachunku lambda jako systemie logicznym / aksjomatycznym, co daje ci niezwykle formalną, podstawową wersję obliczeń.

Maszyny Turinga są przydatne, ale ich podstawowe definicje wymagają posiadania koncepcji zestawów, funkcji itp. Zakłada się, że zbudowano znacznie więcej matematyki.

Z drugiej strony rachunek Lambda jest zdefiniowany w kategoriach logiki, więc można go używać bez większego znaczenia w definicjach teorii mnogości, funkcji itp.

Przepisywanie terminów, wzorowane na logice, nie dotyczy tylko programowania funkcjonalnego. Kiedy przeprowadzasz formalną weryfikację sprzętu lub oprogramowania, zawsze będziesz przeprowadzać jakieś rozumowanie, a to rozumowanie można modelować poprzez przepisywanie terminów.

jmite
źródło
2

Jednym z bardzo praktycznych powodów jest to, że prowadzi do budowy systemów transformacji programów , narzędzi, które pozwalają manipulować kodem programów jako terminy (abstrakcyjne drzewa składniowe) przy użyciu przepisywania składni powierzchniowych.

Jednym z przykładów tego mojego systemu jest DMS Software Reengineering Toolkit , który został wykorzystany do szerokiej gamy analiz programów i ogromnych zadań transformacyjnych. Możesz zobaczyć, jak DMS wyraża ponowne zapisywanie . Te przepisywania są stosowane przez asocjacyjno-przemienny system przepisywania terminów, który działa za kulisami.

Ira Baxter
źródło