История изменений

Задачу свою опиши подробнее пожалуйста.

Я бы хотел разобраться, для чего и как можно использовать лямбда-исчисление. Моя задача - вправить себе мозги, чтобы начать спать спокойно, а не мучаться тем, что я чего-то не понимаю.

Говорят, что при помощи этого исчисления можно описать семантику чего-нибудь. Вот я и решил попробовать описать байт. Структура как структура, по аналогии можно было бы описать что-нибудь ещё, например int, float, double.

И пока что не получается (понять).

Можешь ввести просто такой литерал «байт», операции какие нибудь аксиоматически ввести.

Не могу, не умею. Мне непонятны слова «аксиоматически», «литерал», «ввести». Если я сделаю типизированное исчисление, то это мне добавит проверку типа (чтобы байты не путались с чем-то ещё), но не добавит работоспособности. Т.е. если бы это заработало в типизированном λ-исчислении, то оно точно так же заработало бы и в бестиповом λ-исчислении (только без лишних проверок).

Если я буду что-то лишнее в чистое λ-исчисление вводить, я боюсь, что у меня получится lisp. А мне такое не надо.

Задачу свою опиши подробнее пожалуйста.

Я бы хотел разобраться, для чего и как можно использовать лямбда-исчисление. Моя задача - вправить себе мозги, чтобы начать спать спокойно, а не мучаться тем, что я чего-то не понимаю.

Говорят, что при помощи этого исчисления можно описать семантику чего-нибудь. Вот я и решил попробовать описать байт. Структура как структура, по аналогии можно было бы описать что-нибудь ещё, например int, float, double.

И пока что не получается (понять).

Можешь ввести просто такой литерал «байт», операции какие нибудь аксиоматически ввести.

Не могу, не умею. Мне непонятны слова «аксиоматически», «литерал», «ввести». Если я сделаю типизированное исчисление, то это мне добавит проверку типа (чтобы байты не путались с чем-то ещё), но не добавит работоспособности. Т.е. если бы это заработало в типизированном лямбда-исчислении, то оно точно так же заработало бы и в бестиповом лямбда-исчислении (только без лишних проверок).

Если я буду что-то личшее в чистое лямбда-исчисление вводить, я боюсь, что у меня получится lisp. А мне такое не надо.