ΑZ
вот написал ты квиксорт с переменной-функцией которая определяет по какому полю сортировать
Size: a a a
2021 May 26
ΑZ
где тут бесполезность?*
ΑZ
сцуко я 1.5 часа как спать собирался :/
ΑZ
зацепили меня
AN
ну я тоже.
ΑZ
есть некоторое множество примитивных операций аксиом
AN
но интересно получается. спасибо что рассказываешь.
ΑZ
те же Z и S
TK
Если они делают что-то полезное, значит, в переменной лежало значение типа полезной лямбды, значит, её можно было сконструировать по определению терма, и получается, что полезные лямбды на нижнем уровне могут состоять только из бесполезных лямбд, противоречие
B
спокойной ночи, шо сказать, было интересно
ΑZ
если в двух словах
ΑZ
то термы тебе помогают описывать как ведут себя функции
ΑZ
напоминю
ΑZ
что у нас есть термы, которые имеют типы, которые имеют кайнды
ΑZ
если убрать термы то остаются только типы и кайнды
ΑZ
у функций суммирования и вычитания тип одинаковый
ΑZ
но очевидно разное поведение
AN
а шо там есть теорема про то что лямбда калькулюс описывает все что нужно. поэтому этой примитивной модели достаточно для построения теории?
ΑZ
отсюда: нехватает нам только типов. нужны термы
ΑZ
тезис черча про примитивно-рекурсивные, вычислимые и машины тьюринга