МБ
А можете продемонстрировать, как это сделать? Это, действительно, очень концептуальное заявление. Мне бы очень помогло в моей работе.
Size: a a a
2021 May 08
B
И мы можем выводить формулы пи-исчисления, не смотря на то, какая у них задана человеческая интерпретация.
B
Собственно, пи-исчисление может быть описано как теория только в том случае, если оно образует множество формул, замкнутое относительно коллекции правил вывода.
МБ
А... В этом смысле. Но когда вы строите ЯП, кроме вывода формул нужна семантика.
МБ
Семантику в lambda-исчисление погрузить можно, но это будет огрызок семантики.
B
Ну здесь это будет некоторая модель самого лямбда-исчисления (например, Даны Скотта) плюс некоторые ограничения, которые устанавливает пи-исчисление, когда мы хотим рассматривать только вывод относительно пи-исчисления, и собственные модельные конструкции для описания работы его предикатов.
МБ
Каких предикатов?
МБ
Мне не хватает конкретики. Можете показать, как это сделать?
B
Ну, под таковым можно рассматривать, например, ||
просто некоторый двух/более-местный символ, который можно читать как некоторое утверждение о двух или более индивидах (в данном случае ограничивается до процессов).
просто некоторый двух/более-местный символ, который можно читать как некоторое утверждение о двух или более индивидах (в данном случае ограничивается до процессов).
МБ
Ну, хорошо. А что дальше?
B
Ну, собственно, всё
МБ
Как задать семантику?
B
Переслано от Brenoritvrezorkre
Ну здесь это будет некоторая модель самого лямбда-исчисления (например, Даны Скотта) плюс некоторые ограничения, которые устанавливает пи-исчисление, когда мы хотим рассматривать только вывод относительно пи-исчисления, и собственные модельные конструкции для описания работы его предикатов.
МБ
Ну, то есть, нужно чуть больше, чем само лямбда-исчисление?
B
Модель лямбда-исчисления + ограничения на неё, чтобы не работать не с пи-исчислением + модельные конструкции для предикатов (если мы хотим описать их семантику, но мы можем просто сказать, что они семантически примитивны, а их содержание определяется просто набором правил вывода формул с ними).
МБ
Ну, то есть, как ни крути, а добавить кое-что придётся? Ну, и как бы, тогда вопрос: а зачем тогда lambda-исчисление в этом коктейле, если оно через pi выражается.
B
Это пи здесь выражается через лямбда-исчисление
МБ
Как именно? Вы же сами говорите, что придётся добавить новые домены или дополнительные правила вывода.
МБ
Или я чего-то не понимаю?
B
Мы можем логику предикатов описать через соответствующие собственные правила вывода в терминологии лямбда-исчисления, но это вообще никак не значит такой странности, что мы выразили лямбда-исчисление в логике предикатов.