EG
Да, это значит, что если
x — unit, то вместо f x можно подставить unitf x это юнит если x — unitSize: a a a
2020 October 16
b
это не типы
b
в логосе нет типов
b
когда ты говоришь
unit := iota ты не создаешь типEG
«Если для
x верно утверджение x := unit_t., то вместо f x можно подставить unit»b
когда ты говоришь
-> unit ты присваиваешь не тип функции, а буквально показываешь на конкретный знак, unitEG
когда ты говоришь
-> unit ты присваиваешь не тип функции, а буквально показываешь на конкретный знак, unitДа, я понимаю
b
«Если для
x верно утверджение x := unit_t., то вместо f x можно подставить unit»ну хорошо да
EG
Для
f f f будет экспоненциально много способов это выполнитьb
ну так оно и не посчитается
b
ты удивишься, но если начнешь строить гиперграф пропозициональной формы этого высказывания
EG
Почему? Это, например, корректное выражение по правилу
x f y.b
то очень быстро найдешь там циклы и только циклы
b
когда начнешь делать подстановки
b
Почему? Это, например, корректное выражение по правилу
x f y.потому что есть более одного корректного способа трактовать это выражение
b
ты вообще предложил циклический случай
b
когда пропозиции разворачиваются одна в другую
EG
потому что есть более одного корректного способа трактовать это выражение
У меня просто есть ощущение, что в любой нетривиальной программе будет несколько корректных способов трактовать большую часть выражений
b
это не так
b
или как я сказал бы это ложное ощущение