Re[3]: Основы лямбда-исчисления
От: ShcheknItrch  
Дата: 13.01.10 12:21
Оценка:
Здравствуйте, Mr.Cat, Вы писали:

MC>Здравствуйте, ShcheknItrch, Вы писали:

SI>>Ну вот объясните, что тогда понимается под функцией, есть ли такое понятие, как область определения, на которой задан аргумент, и во что отображает эта функция.
MC>ЛИ — это, если можно так выразиться, символьная система. Она изучает символы, как из них можно записывать выражения и как эти выражения потом можно комбинировать и переписывать. Понятия "функция", "число" и т.п. к ЛИ не относятся — мы их применяем к определенным выражениям неформально, на основании интуитивного сходства.

SI>>2.1.1. Определение. (i) Ламбда-термы будут словами в следующем алфавите:

SI>> v0, v1, ... переменные
SI>> λ абстрактор
SI>> ( , ) скобки.
SI>> (iii) Множество Λ ламбда-термов (или, что то же, λ-термов) индуктивно определяется следующим образом:
SI>> (1) x Є Λ;
SI>> (2) M Є Λ -> (λxM) Є Λ;
SI>> (3) M, N Є Λ -> (MN) Є Λ,
SI>>где x в (1) и (2) — произвольная переменная.

SI>>Ведь если у нас изначально есть только одни лишь лямба-термы, то мы можем только лишь их комбинировать, а вот под применением функции к аргументу можно понимать только лишь применение одного лямбда-терма к другому. Тут под применением нужно понимать простое комбинирование.

SI>>...
SI>>Правильно ли понимать MN просто как упорядоченный набор лямбда-термов M и N. И правильно ли это называть применением M к N?
MC>Какое такое простое комбинирование? Нет простого комбинирования и упорядоченных наборов. Есть три правила формирования термов.

SI>>Т.е. выходит так, что сначала дается определение лямбда-абстракции с использованием понятия аппликации, т.е. привлекая понятие функции (определения которого еще не было дано). Далее дается определения лямбда-термам и процессу их индуктивного построения.

MC>Забудь про функции. Все в ЛИ — набор символов. Абстракция — набор символов из правила (2) цитаты выше. Аппликация — набор символов из правила (3).

SI>>Но что меня смущает — так это то, что в определение лямбда-термов входит лямбда-абстрактор, который понимается как (см. первый пост):

MC>Нет, не входит (если ты имеешь в виду просто буковку "λ"). Он входит в алфавит, словами в котором являются термы.


Спасибо. Все же тяжело разбираться, когда в явном виде не всегда указано, что именно используется неформально (на основании интуитивного сходства), а что следует воспринимать как определения или аксиомы. Впрочем, возможно, это проблемы моего восприятия.
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.