AG
но из них сложно выжать код
Size: a a a
2020 October 23
DF
А, понял
AG
конструктивная логика сложнее в использовании, но она по карри-говарду сразу имеет вычислительную интерпретацию
DF
Отлично
AG
вот идея программирования на пруверах это переход к 100% конструктивным методам
DF
А это можно считать аналогом пролога?
AG
ссрефлект кстати, на котором я выше скидывал код это интересный промежуточный вариант
DF
Логического программирования?
AG
там используются классические приемы внутри конструктивного сеттинга
AG
потому что это фреймворк в первую очередь для доказательств над конечными и разрешимыми структурами
DF
Очень познавательно
AG
для которых работает закон исключенного третьего, который собственно и является определением разрешимости
AG
формула A разрешима, если существует алгоритм строящий
A \/ ~ADF
Ааа получается если бы у нас был карри Говард между классической логикой то все было бы разрешимо?
AG
Dollar Føølish
А это можно считать аналогом пролога?
в пруверах используются техники логического программирования, но они много где используются
DF
Правда ведь?
AG
те же тайпклассы и имплициты это ЛП
AG
Dollar Føølish
Ааа получается если бы у нас был карри Говард между классической логикой то все было бы разрешимо?
ну это вопрос структуры реальности :)
DF
А расскажите вкрации
DF
Если не трудно