Лямбда-исчисление — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 73: Строка 73:
 
а <tex>\lambda x \to \lambda y \to y z</tex> и <tex>\lambda y \to \lambda x \to y z</tex> {{---}} нет.
 
а <tex>\lambda x \to \lambda y \to y z</tex> и <tex>\lambda y \to \lambda x \to y z</tex> {{---}} нет.
  
−
\subsection{$\beta$-редукция}
+
===<tex>\beta</tex>-редукция===
−
$\beta$-редукция олицетворяет идею счёта значения функции. Выражение вида
 
−
|(\x -> f) y| можно заменить на $f[x := y]$, где $f[x:=y]$, как и ранее, означает
 
−
замену всех свободных вхождений $x$ в $f$ на $y$.
 
  
−
Через $f \to_\beta g$ обозначают сведение $f$ к $g$ с помощью одной $\beta$-редукции.
+
{{Определение
−
А через $f \to_\beta^* g$~--- за ноль или более.
+
|definition=
 +
<tex>\beta</tex>-редукция олицетворяет идею счёта значения функции. Выражение вида
 +
<tex>(\lambda x \to f) y</tex> можно заменить на <tex>f[x := y]</tex>, где <tex>f[x:=y]</tex>, как и ранее, означает
 +
замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
 +
}}
 +
 
 +
{{Определение
 +
|definition=
 +
Через <tex>f \to_\beta g</tex> обозначают сведение <tex>f</tex> к <tex>g</tex> с помощью одной <tex>\beta</tex>-редукции.
 +
А через <tex>f \to_\beta^* g</tex>~--- за ноль или более.
 +
}}
  
 
\subsection{$\eta$-редукция}
 
\subsection{$\eta$-редукция}

Версия 14:38, 6 декабря 2012

Эта статья находится в разработке!

Лямбда-исчисление

Лямбда-исчисление — формальная система, придуманная в 1930-х годах Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. Эта концепция показала себя удобной и сейчас активно используется во многих языках программирования.

Более формально, лямбда-функцию (или, лямбда-терм) можно задать следующей грамматикой:

Определение:
[math] \begin{array}{r c l} \langle Term \rangle & ::= & \langle Variable \rangle \\ & || & \langle Term \rangle \langle Term \rangle \\ & || & \lambda \langle Variable \rangle \to \langle Term \rangle\\ & || & ( \langle Term \rangle )\\ \langle Variable \rangle & ::= & \langle Char \rangle *\\ \end{array} [/math]


В первом случае функция является просто переменной. Во втором происходит аппликация (применение) одной функции к другой. Это аналогично вычислению функции-левого операнда на аргументе-правом операнде. В третьем — абстракция по переменной. В данном случае происходит создание функции одного аргумента с заданными именем аргумента и телом функции.

Рассмотрим, например, функцию [math]id = \lambda x \to x[/math]. Эта функция принимает аргумент и возвращает его неизменённым. Например, [math]id 2 \equiv 2[/math]. Аналогично, [math]id y == y[/math].

Ещё один пример функции: [math]sum = \lambda x \to \lambda y \to x + y|. Эта функция двух аргументов, которая возвращает их сумму. Правда, здесь мы немного вышли за написанную выше грамматику. Ну да ладно. \lt tex\gt sum 2 3 == 5[/math]

Приоритет операций

  • Применение левоассоциативно: [math]x y z w == ((x y) z) w[/math]
  • Аппликация забирает себе всё, до чего дотянется: [math]\lambda x \to \lambda y \to \lambda z \to z y x \equiv \lambda x \to (\lambda y \to (\lambda z \to ((z y) x)))[/math]
  • Скобки играют привычную роль группировки действий

Свободные и связанные переменные

Связанными переменными называются все переменные, по которым выше в дереве разбора были абстракции. Все остальные переменные называются свободными.

Например, в [math]\lambda x \to \lambda y \to x[/math], [math]x[/math] связана, а [math]y[/math]— свободна. А в [math]\lambda y \to x (\lambda x \to x)[/math] в своём первом вхождении переменная [math]x[/math] свободна, а во втором — связана.

Рассмотрим функции [math]\lambda y \to y[/math] и [math]\lambda x \to y[/math]. В первой из них при взгляде на [math]y[/math] понятно, что она имеет отношение к переменной, по которой производилась абстракция. Если по одной и той же переменной абстракция производилась более одного раза, то переменная связана с самым поздним (самым нижним в дереве разбора) абстрагированием. Например, в [math]\lambda x \to \lambda x \to \lambda y \to \lambda x \to x[/math], переменная [math]x[/math] связана с самой правой абстракцией по [math]x[/math].

[math]\alpha[/math]-конверсия

Рассмотрим функции [math](\lambda x \to x) z[/math] и [math](\lambda y \to y) z[/math]. Интуитивно понятно, что они являются одинаковыми.


Определение:
[math]\alpha[/math]-конверсия — переименование связанной переменной. Выражение

[math]\lambda x \to f[/math] можно заменить на [math]\lambda y \to f[x := y][/math], если [math]y[/math] не входит свободно в [math]f[/math], где [math]f[x:=y][/math] означает замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].

Функции, получающиеся одна из другой с помощью [math]\alpha[/math]-конверсий, называются [math]\alpha[/math]-эквивалентными и обозначаются [math]f \equiv_\alpha g[/math].

Функции [math]\lambda x \to \lambda y \to x y z[/math] и [math]\lambda a \to \lambda x \to a x z[/math] являются [math]\alpha[/math]-эквивалентными, а [math]\lambda x \to \lambda y \to y z[/math] и [math]\lambda y \to \lambda x \to y z[/math] — нет.

[math]\beta[/math]-редукция

Определение:
[math]\beta[/math]-редукция олицетворяет идею счёта значения функции. Выражение вида

[math](\lambda x \to f) y[/math] можно заменить на [math]f[x := y][/math], где [math]f[x:=y][/math], как и ранее, означает

замену всех свободных вхождений [math]x[/math] в [math]f[/math] на [math]y[/math].


Определение:
Через [math]f \to_\beta g[/math] обозначают сведение [math]f[/math] к [math]g[/math] с помощью одной [math]\beta[/math]-редукции. А через [math]f \to_\beta^* g[/math]~--- за ноль или более.


\subsection{$\eta$-редукция}

Рассмотрим выражение вида
\rangle$. При этом, голова списка будет храниться как показатель степени при $p_{len}$.

\begin{code} empty = pair' `App` zero' `App` one' cons = Lam "h" $ Lam "t" $ pair' `App` (succ' `App` (fst `App` Var "t")) 

       `App` (mult' `App` (snd `App` Var "t") `App` (power' 
               `App` (ithPrime `App` (fst `App` Var "t"))
               `App` Var "h"
       ))

head = Lam "list" $ getExponent `App` (snd `App` Var "list") 

                               `App` (ithPrime `App` (pred' `App` (fst `App` Var "list")))

tail = Lam "list" $ pair' `App` (pred' `App` (fst `App` Var "list")) 

                         `App` (eliminateMultiplier `App` (snd `App` Var "list")
                                 `App` (ithPrime `App` (pred' `App` (fst `App` Var "list" )))
                               )

eliminateMultiplier' = Lam "f" $ Lam "n" $ Lam "m" $ if `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m")) 

                       `App` (Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m")
                       `App` Var "n"

eliminateMultiplier = fix' `App` eliminateMultiplier'

getExponent' = Lam "f" $ Lam "n" $ Lam "m" $ if `App` (isZero' `App` (mod' `App` Var "n" `App` Var "m")) 

               `App` (succ' `App`(Var "f" `App` (div' `App` Var "n" `App` Var "m") `App` Var "m"))
               `App` zero'

getExponent = fix' `App` getExponent' \end{code}

На основе этого всего уже можно реализовать эмулятор машины тьюринга: с помощью пар, списков чисел можно хранить состояния. С помощью рекурсии можно обрабатывать переходы. Входная строка будет даваться, например, закодированной аналогично списку: пара из длины и числа, характеризующего список степенями простых. Я бы продолжил это писать, но уже на операции $head [1, 2]$ я не дождался окончания выполнения. Скорость лямбда-исчисления как вычислителя печальна.

\ignore{ \begin{code}

four' = norm $ succ' `App` three' five' = norm $ succ' `App` four'

list2 = norm $ cons `App` one' `App` empty list32 = cons `App` zero' `App` list2

normFiveFact = normIO 0 $ fact' `App` five'

-- fiftysix = mult twentyeight two -- fiftyfive = pred fiftysix -- six = pred seven

--main = do print $ fiftysix (+1) 0 main = do 

--   f <- normIO 0 $ ithPrime `App` three'
--   f <- normIO 0 $ getExponent `App` (norm $ plus' `App` four' `App` four') `App` two'
   f <- normIO 0 $ head `App` (tail `App` list32)
   print $ toInt f

\end{code} }

\end{document} [1]

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Лямбда-исчисление&oldid=27280»