#import "@local/common:0.0.0": *
#import "@local/theorem:0.0.0": *
#show: theorem
#import "./template.lib.typ": *
#show: formatting
#set heading(numbering: none)
#set text(size: 13pt)
#set page(background: image("pictures/troubles-faded.jpg", width: 100%, height: 100%, fit: "stretch"))

#head([ Итоговая работа, II вариант ])

== На 3:

+ Дайте определение _комбинатора неподвижной точки._ Приведите примеры. Докажите, что выражение $#Y _M == @f.. (@x%y.. f(x x y))(@x%y.. f(x x y))M$ является комбинатором неподвижной точки для любого $M in #L$.

+ Дайте определение _чисел Барендрегта_ и _чисел Чёрча._ Постройте л-выражения $H$ и $H^(-1)$, которые переводят одни в другие: $H nums(n) = c_n$, #h(5pt) $H^(-1) c_n = num(n)$.

+ Дайте определение л-представимости числовой функции. Определите функцию _суперпозиции_ для числовых функций $chi, psi_1, psi_2, ..., psi_k$. 

+ Покажите, что функция $#Am == @x%y%z.. x(y z)$ задаёт умножение на числах Чёрча: $#Am c_n c_m = c_(n m)$.

== На 4:

+ Докажите, что класс л-представимых функций замкнут относительно минимизации.

+ Определите понятие _адекватной числовой системы._ Докажите, что числовая система $d = (d_0, #S^+_d)$ адекватна в том и только том случае, когда она имеет оператор предшествующего элемента $#P^-_d$: #h(5pt) $#P^-_d #h(2pt) d_(n+1) = d_n, hs forall n in NN_0$.

+ Докажите _обобщённую теорему о неподвижной точке:_ $forall F_1, F_2, ..., F_n in #L: hs exists X_1, X_2, ..., X_n in #L:$
  $
    X_1 &= F_1 X_1 X_2 ... X_n,\
    X_2 &= F_2 X_1 X_2 ... X_n,\
    dots.v\
    X_n &= F_n X_1 X_2 ... X_n.\

  $

== На 5:

+ Докажите теорему Скотта-Карри о неразрешимости.

+ Покажите, что следующие две последовательности являются адекватными числовыми системами:\
  [a]#hs $d = (#Y, @x.. [x, P])$, где $P in #L$ произвольно;\
  [b]#hs $e = (#K, @x.. [x, #Y])$.\
  (подсказка: для $d$ используйте $#Zero _d == [#K (#K #K), #I]$)

+ Покажите, что функция $"id" : NN_0 -> NN_0, hs "id"(n) = n$ является рекурсивной. Покажите, что всякий многочлен
  $
    &P : NN_0 -> NN_0,\
    P(n) &= a_0 + a_1 n + a_2 n^2 + ... + a_k n^k,
  $
  с коэффициентами $a_0, a_1, ..., a_k in NN_0$, --- рекурсивная функция.
