deep-econom (deep_econom) wrote,
deep-econom
deep_econom

Category:
https://ru.wikipedia.org/wiki/Исчисление_конструкций
Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов

https://ru.wikipedia.org/wiki/Кодирование_Чёрча
https://ru.wikipedia.org/wiki/Формальная_система

Ну может не в таком жутком виде, но в адаптированном эти вещи вроде как подходят для исчисления моделей.
Имеется ввиду сама идейная часть. Надо думать.
На самом деле остенсивные определения по сути соответствуют константам в абстрактном языке (абстрактной формальной системе) "конкретная данная кошка", кошка это уже тип данных, а также может соответствовать типизированной переменной и т.п.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 2 comments