Слабое отношение следования между \(\lambda\)-термами

Main Article Content

В. И. Шалак

Аннотация

Язык \(\lambda \)-исчисления находит широкое применение для решения задач в логике, информатике, лингвистике и искусственном интеллекте. Само \( \lambda \)-исчисление строится вокруг базисного отношения между термами, которое называется \( \beta \)-редукцией. В предлагаемом докладе для типизированного в смысле Карри \( \lambda \)-исчисления формулируется более слабое отношение между термами, которое может как иметь самостоятельное значение, так и позволить установить более тонкие связи между логикой и \( \lambda \)-исчислением. Основная идея заключается в том, что при приписывании терму X типа \( \alpha \) относительно контекста \( \varGamma \), что записывается в виде \( \varGamma \vdash X:\alpha \), понятие контекста играет роль, аналогичную понятию модели в логике. Если в логике выражение \( M \vDash A \) означает, что формула \( A \) истинна в модели \( M \), то в типизированном \(\lambda \)-исчислении выражение \( \varGamma \vdash X:\alpha \) означает, что в контексте \( \varGamma \) терму \( X \) приписан тип \( \alpha \), и этот терм имеет значение, которое может быть вычислено. В логике отношение следования между формулами \( A \) и \( B \) определяют как \( A\vDash B \Leftrightarrow \forall M(M\vDash A \Rightarrow M\vDash B) \). Если перенести эту схему в \( \lambda \)-исчисление, то отношение \( \lambda \)-следования между темами может быть определено как \( X \vDash _{\lambda} Y \Leftrightarrow \forall \varGamma \in Ctx [\exists\alpha(\varGamma \vdash X:\alpha) \Rightarrow \exists\beta(\varGamma \vdash Y:\beta)] \). Смысл этого отношения заключается в том, что в каждом контексте, в котором терму \( X \) может быть приписан некоторый тип, терму \( Y \) также может быть приписан некоторый тип. Иными словами, если вычислима функция, представленная термом \( X \), то вычислима функция, представленная термом \( Y \). Отношение \( \lambda \)-следования обладает многими свойствами, присущими классическому отношению следования между формулами логики, а также рядом новых свойств, характерных для \( \lambda \)-исчисления с типами.

Скачивания

Данные скачивания пока не доступны.

Article Details

Как цитировать
[1]
В. И. Шалак. Слабое отношение следования между \(\lambda\)-термами // Логические исследования / Logical Investigations. 2019. Т. 24. № 2. С. 151-157.
Раздел
I Конгресс Русского общества истории и философии науки. Материалы по логике
Биография автора

В. И. Шалак, Институт философии РАН

Российская Федерация, 109240, г. Москва, ул. Гончарная, д.12, стр.1