B
или нет, или да
Size: a a a
2021 May 26
ΑZ
ну типа ими полезно моделировать
AN
не совсем. блин число должно быть функцией.
TK
Но термы не функции, и функции на них выразить невозможно
ΑZ
add a Z = a
add a (S n) = (S a) nTK
А с их помощью типа пожалуйста
ΑZ
кроме функций нужны данные чтобы ими оперировать
ΑZ
аргумент лямбды это переменная
ΑZ
без аргумента функцию ты не напишешь
B
а 0 это кто
ΑZ
например для определения функции add мне нужна переменная a
ΑZ
a - переменная
0 - константа Z
0 - константа Z
B
а все да, аксиома вообще не про то
ΑZ
тут не нужна аксиома, я могу определить функцию Add
B
да, я про то же
TK
Но лямбды могут звать только другие лямбды или термы, которые иногда внезапно стрелки (не путать с лямбдами), и их значение получено магией
ΑZ
лямбды это стрелки
ΑZ
я тебе фигню сказал
ΑZ
там полноценное определение
AN
что за стрелки? я пропустил что-то.