3622
правки
Изменения
→Лямбда-исчисление
== Лямбда-исчисление==
{{Определение
|definition=
'''Лямбда-выражением''' (англ. <tex>\lambda</tex>''-term'') называется выражение, удовлетворяющее следующей грамматике:<br>
<tex>
\Lambda \to V\\
\Lambda \to \Lambda @ \ \Lambda\\\Lambda \to \lambda V . \Lambda\\
</tex>
где <tex>V</tex> {{---}} множество всех строк над фиксированным алфавитом <tex> \Sigma \setminus \{ "\lambda", "\ ",\ "."\} </tex>.
}}
В первом случае функция является просто переменной.
|definition=
'''Каррирование''' (англ. ''carrying'') {{---}} преобразование функции от многих переменных в функцию, берущую свои аргументы по одному. Для функции <tex>h</tex> типа <tex>h\ :\ (A\ *\ B)\ \to\ C</tex> оператор каррирования <tex>\Lambda </tex> выполняет преобразование <tex>\Lambda (h)\ :\ A\to (B\to C)</tex>. Таким образом <tex>\Lambda (h)</tex> берет аргумент типа <tex>A</tex> и возвращает функцию типа <tex>B\ \to\ C</tex>. С интуитивной точки зрения, каррирование функции позволяет фиксировать ее некоторый аргумент, возвращая функцию от остальных аргументов. Таким образом, <tex>\Lambda</tex> представляет собой функцию типа <tex>\Lambda :\ (A\ *\ B\to C)\to (A\to (B\to C))</tex>.
}}
==Нотация Де Брёйна==
