Числення контекстних термів для систем переписування
У статті пропонується числення контекстних термів, що доповнює традиційний апарат алгебраїчних сигнатур, котрі використовуються в системах переписування термів, конструкціями роботи з контекстом: утворення контексту, визначення контекстного значення та зв’язку терму з контекстом із перевіркою відпов...
Gespeichert in:
| Datum: | 2018 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут програмних систем НАН України
2018
|
| Schriftenreihe: | Проблеми програмування |
| Schlagworte: | |
| Online Zugang: | http://dspace.nbuv.gov.ua/handle/123456789/144579 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Числення контекстних термів для систем переписування / P.C. Шевченко // Проблеми програмування. — 2018. — № 2-3. — С. 21-30. — Бібліогр.: 12 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| Zusammenfassung: | У статті пропонується числення контекстних термів, що доповнює традиційний апарат алгебраїчних сигнатур, котрі використовуються в системах переписування термів, конструкціями роботи з контекстом: утворення контексту, визначення контекстного значення та зв’язку терму з контекстом із перевіркою відповідності. Це дозволяє сформулювати задачі, пов’язані з аналізом та трансформаціями програмного коду, у більш природньому вигляді, оскільки структура вихідного коду в сучасних мовах програмування також має ієрархічну контекстну структуру, що може прямо відповідати структурі терму в переписувальному правилі. Правила виводу типів для мови програмування можуть бути представлені як правила задовільності контексту. Таким чином можна отримати досить простий механізм, що об’єднує переписування термів з аналізом контексту. Застосування підходу описано на прикладі моделювання системи типів сучасних мов програмування: від обмежень на значення до лінійної типізації. |
|---|