Изменения

Здесь <tex>n s z</tex> {{---}} <tex>n</tex> раз применённая к <tex>z</tex> функция <tex>s</tex>. Но нужно применить <tex>n+1</tex>

\subsection{===Сложение}===Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить неединицу, а второе число.

<tex>\beginoperatorname{codeplus}plus' = Lam "\lambda n" $ Lam "\to \lambda m" $ Lam "\to \lambda s" $ Lam "\to \lambda z" $ Var "\to n" `App` Var "s" `App` (Var "m" `App` Var "s" `App` Var "z")\end{code}</tex>

<tex>n<$n$ /tex> раз применить $<tex>s$ </tex> к применённому $<tex>m$ </tex> раз $<tex>s$ </tex> к $<tex>z$></tex>

|<tex>(plus three three) (+1) 0 == | \evaloperatorname{(plus three three} \bar 3 \bar 3) (+1) 0}\equiv 6</tex>

\subsection{===Умножение}===

функции должна быть не $<tex>s$</tex>, а функция, применяющая $<tex>n$ </tex> раз $<tex>s$</tex>.

<tex>\beginoperatorname{codemult}mult' = Lam "\lambda n" $ Lam "\to \lambda m" $ Lam "\to \lambda s" $ Var "\to n" `App` (Var "m" `App` Var "s")\end{code}</tex>

Здесь |<tex>m s|~</tex> {{--- }} функция, которая $<tex>m$ </tex> раз применит $<tex>s$ </tex> к тому, что дадут ей на вход. С помощью $<tex>\eta$</tex>-редукции можно немного сократить эту формулу

<tex>\beginoperatorname{specmult}mult = \lambda n -> \to \lambda m -> \to \lambda s -> \to n (m s)\end{spec}</tex>

|<tex>(mult three three) (+1) 0 == | \evaloperatorname{(mult three three} \bar 3 \bar 3) (+1) 0}\equiv 9</tex>