где Y є lh.(lx.h(xx))(lx.h(xx)) - конструктор неподвижной точки, x,h О V.    Мы будем широко использовать следствие теоремы Чёрча - Россера (CR-теоремы), утверждающее, что для любого терма t О L имеют место следующие два утверждения:

   Мы также будем использовать теорему о замене для b-равенства, которая состоит в следующем: пусть t_t1 есть терм с фиксированным вхождением подтерма t₁, а t_t2 - терм, полученный из терма t_t1 в результате замены фиксированного вхождения подтерма t₁ на терм t₂, тогда t₁ = t₂ Ю  t_t1 = t_t2.
   2. Уравнения с отделяющейся переменной и свойства их решений. Рассмотрим уравнение

где t⁰[f] є f,    t^m[f] є t[t^m-1[f]],    m і 1.
   Перед тем как перейти к непосредственному доказательству теоремы 1, введем одно понятие и докажем лемму 1.
   Пусть t[f] О L,   f О V,   FV(t[f]) = {f} и не существует такого tў О L⁰, что t[f] ®® tў. Всякий терм вида (lx.t₁[xx])(lx.t₂ [xx]), где x О V,    t₁,t₂ О L,   t[f] ®® t₁[f],    t[f] ®® t₂ [f], назовем ядром. Одношаговую редукцию назовем ядерной, если её редексом является ядро.
   Лемма 1. Пусть t[f] О L,   f О V,   FV(t[f]) = {f} и не существует такого tў О L⁰, что t[f] ®® tў. Пусть О L,   y О V,  [(lx.t[xx])(lx.t[xx])] ®® t₀, где t₀ О NF⁰ и число ядерных редукций равно r і 0. Тогда [tⁿ[f]] ®® t₀, если n і r.
   Доказательство леммы следует из утверждения 1.
   Утверждение 1. Пусть t[f] О L,   f О V,  FV(t[f]) = {f} и не существует такого tў О L⁰, что t[f] ®® tў.
   Пусть О L,   y О V и є {y, ј , y}, где число свободных вхождений переменной y в терм равно k і 0.
   Пусть t_i[f],  t_iў[f] О L, t[f] ®® t_i [f],    t[f] ®® t_iў[f],   i = 1, ј , k, и {(lx.t₁[xx])(lx.t₁ў[xx]), ј , (lx.t_k[xx])(lx.t_kў[xx])} ®® t₀, где t₀ О NF⁰ и число ядерных редукций, редексы которых получены в процессе редукции из подставленных в терм {y, ј , y} ядер, равно r і 0.
   Тогда {t^n₁[f], ј ,  t^n_k[f]} ®® t₀, если n_i і r,   i = 1, ј , k.
   Доказательство. Пусть r = 0, тогда очевидно, что {t^n₁ [f], ј , t^n_k[f]} ®® t₀. Пусть r > 0 и утверждение 1 верно для r - 1. Докажем для r. Легко видеть, что имеет место следующее:

{(lx.t1[xx])(lx.t1ў[xx]),ј,(lx.tk[xx])(lx. tkў[xx])} ®® _ t¢1   {(lx . _ t¢1   [xx])(lx . _ t¢1   [xx]), ј , (lx . _ ti   [xx])(lx . _ t¢   [xx]),ј,(lx . _ ts   [xx])(lx . _ t¢s   [xx])},

где (lx .[xx])(lx .[xx]), i = 1, ј , s, s і 1, есть все ядра, полученные в процессе редукции из ядер, подставленных в терм {y,ј,y}, и число ядерных редукций, редексами которых являются такие ядра, равно 0. Далее мы фиксируем момент первой интересующей нас ядерной редукции:

где n^ў_i О { n₁,ј, n_k} , i = 1,ј,s, s і 1. Далее имеем: { t^nў₁[f],ј,t^nў_i[f],ј,t^nў_s[f]} ®® {t^nў₁[f],ј,[t^nў_i-1[f]],ј,t^nў_s[f]} є {t^nў₁[f],ј,t^nў_i-1[f],ј,t^nў_i-1[f],ј,t^nў_s[f]} ®® (по предположению индукции) ®® t₀.
   Утверждение 1 доказано.
   Доказательство теоремы 1. (Ь) Пусть tⁿ[f]n₁n₂јn_k ®® t₀ для некоторого n > 0. Тогда, как легко видеть, tⁿ[t]n₁n₂јn_k ®® t₀. Так как t - решение уравнения (1), то t = tⁿ[t],    tn₁n₂јn_k = tⁿ[t]n₁n₂јn_k, и по следствию CR-теоремы имеем: tn₁n₂јn_k ®® t₀.
   (Ю) Пусть tn₁n₂јn_k ®® t₀. Возможны два случая:
   a)      $tў О V⁰, t[f] ®® tў,
   b)      Ш$tў О V⁰, t[f] ®® tў.
   Рассмотрим случай (a). Так как t[f] ®® tў и tў О V⁰, то t[t] ®® tў. Так как t - решение уравнения (1), то t = t[t] и tn₁n₂јn_k = t[t]n₁n₂јn_k = tўn₁n₂јn_k. Следовательно, согласно следствию CR-теоремы, tўn₁n₂јn_k ®® t₀. Таким образом, t[f]n₁n₂јn_k ®® tўn₁n₂јn_k ®® t₀, и n = 1.
   Рассмотрим случай (b). Легко видеть, что t є Y(lf.t[f]) є (lh.(lx.h(xx))(lx.h(xx))) (lf.t[f]) ® (lx.(lf.t[f])(xx))(lx.(lf.t[f])(xx)) ®® (lx.t[xx])(lx.t[xx]) ® t[(lx.t[xx])(lx.t[xx])].
   Следовательно, tn₁n₂јn_k = t[(lx.t[xx])(lx.t[xx])]n₁n₂јn_k є [(lx.t[xx]) (lx.t[xx])]. По следствию CR-теоремы имеем: [(lx.t[xx])(lx.t[xx])] ®® t₀, где число ядерных редукций равно некоторому r, r і 0. Пусть n = r + 1. Тогда, согласно лемме 1, имеем:

tn[f]n1n2јnk є t[tn-1[f]]n1n2јnk є[tn-1[f]] ®® t0.

   Теорема 1 доказана.
   Теорема 2. Не существует такого алгоритма, который по каждому уравнению (1) и термам n₁,n₂,ј,n_k О NF⁰, где k і 0, отвечает на вопрос о существовании такого n і 1, при котором терм tⁿ[f]n₁n₂јn_k имеет замкнутую нормальную форму.
   Доказательство. Проблема существования нормальной формы для замкнутого терма, которая является неразрешимой (см. [1]), сводится к рассматриваемой проблеме. Пусть терм t О L⁰. Рассмотрим уравнение f = t[f],    f О V, и возьмем k = 0. Очевидно, что для любого n і 1   tⁿ[f] є t[f], так как терм t замкнут. Следовательно, вопрос о существовании требуемого n эквивалентен вопросу о существовании нормальной формы для терма t. Теорема 2 доказана.
   Теорема 3. Существует алгоритм, который по каждому уравнению (1) и термам n₁,n₂,ј,n_k О NF⁰, k і 0, таким, что терм tⁿ[f]n₁n₂јn_k имеет замкнутую нормальную форму для некоторого n і 1, строит такое n.
   Доказательство следует из теоремы 1 и леммы 1.
   Рассмотрим уравнение (1) и последовательность замкнутых нормальных форм n₁,n₂,ј,n_k,   k і 0. Определим   вычислительную  последовательность t₁[f],ј,t_n[f],ј, состоящую из нормальных форм, которую обозначим Seq(t[f],) (если k = 0, то Seq(t[f]) обозначает ту же последовательность, что и Seq(t[f],)). Последовательность Seq(t[f],) может быть либо пустой, либо конечной, либо бесконечной. В бесконечной последовательности все её члены - незамкнутые нормальные формы. Члены конечной последовательности либо все незамкнуты, либо замкнут только последний её член. Вычислительная последовательность Seq(t[f],) пуста, если терм t[f]n₁n₂јn_k не имеет нормальной формы. Если терм t[f]n₁n₂јn_k имеет нормальную форму, то вычислительная последовательность не пуста и определяется следующим образом:
   t₁[f] есть нормальная форма терма t[f]n₁n₂јn_k. Пусть уже построена подпоследовательность t₁[f],ј,t_i[f],  i і 1, определим, как строится еe продолжение.
   Если t_i[f] О NF⁰ или терм t_i[t[f]] не имеет нормальной формы, то t_i[f] есть последний член вычислительной последовательности.
   Если t_i[f] О NF\NF⁰ и терм t_i[t[f]] имеет нормальную форму, то t_i+1[f] есть нормальная форма терма t_i[t[f]].
   Теорема 4. Пусть дано уравнение (1), его решение (2) и последовательность замкнутых нормальных форм n₁,n₂,ј,n_k,  k і 0, тогда:
   a) eсли вычислительная последовательность Seq(t[f],) конечна и имеет вид t₁[f],ј,t_n[f], где t_n[f] О NF⁰, n і 1, то tn₁n₂јn_k ®® t_n[f];
   b) eсли вычислительная последовательность Seq(t[f],) бесконечна, то терм tn₁n₂јn_k не имеет нормальной формы;
   c) eсли вычислительная последовательность Seq(t[f],) пуста, или конечна и при этом имеет вид t₁[f],ј,t_n[f], где n і 1,  t_n[f] О NF\NF⁰ и терм t_n[t[f]] не имеет нормальной формы, то терм tn₁n₂јn_k может как иметь, так и не иметь нормальную форму.
   Доказательство. (a) Seq(t[f],) есть вычислительная последовательность t₁[f],ј,t_n[f], где:

   Следовательно, согласно теореме 1, tn₁n₂јn_k ®® t_n[f].
   (b) В этом случае вычислительная последовательность t₁[f],ј,t_n[f],ј бесконечна. Покажем, что для любого n і 1 терм tⁿ[f]n₁n₂јn_k имеет незамкнутую нормальную форму. Аналогично пункту (a) имеем: tⁿ[f]n₁n₂јn_k ®® t_n[f], где t_n[f] О NF\NF⁰, n і 1. Таким образом, не существует такого n і 1, что tⁿ[f]n₁n₂јn_k ®® t₀ и t₀ О NF⁰. Следовательно, согласно теореме 1, терм tn₁n₂јn_k не имеет нормальной формы, так как он замкнут.
   (c) Перед доказательством данного пункта введем обозначения для некоторых термов. Пусть x,y О V, тогда:
   I є lx.x,    T є lxy.x,    F є lxy.y,   W є (lx.xx)(lx.xx),
   if t₁ then t₂ else t₃ є t₁t₂ t₃, где t₁,t₂ ,t₃ О L,
   й0щ є I,  йn + 1щ є lx.xFйnщ, где n = 0,1,2,ј,
   Zero є lx.xT,     S⁺ є lyx.xFy,    P^- є lx.xF.
Для каждого t О L терм S⁺t условимся обозначать t⁺, а терм P^-t - t^-.
   Рассмотрим уравнение

где f О V. Легко видеть, что последовательность Seq(W) пуста, так как терм W не имеет нормальной формы. Не имеет нормальной формы и терм t є Y(lf.W) є (lh.(lx.h(xx))(lx.h(xx)))(lf.W) ® (lx.(lf.W)(xx))(lx.(lf.W)(xx)) ®® (lx.W)(lx.W) ® W.
   Рассмотрим уравнение
                         f = lx. if Zero x then lx.I else (fx^-)W є t[f],
где x,f О V. Покажем, что последовательность Seq(t[f], й1щ) пуста.
t[f]й1щ є (lx. if Zero x then lx.I else (fx^-)W)й1щ ®® f й0щW, следовательно, терм t[f]й1щ не имеет нормальной формы. Однако, согласно теореме 1, tй1щ ®® I, так как t²[f]й1щ ®® I. Покажем это: t² [f]й1щ є (lx. if Zero x then lx.I else ((lx. if Zero x then lx.I else (fx^-)W)x^-)W)й1щ ®® ((lx. if Zero x then lx.I else (fx^-)W)й0щ)W ®® (lx.I)W ® I.
   Рассмотрим уравнение
                           f = lx. if Zero x then fx⁺ else W є t[f],
где x,f О V. Покажем, что последовательность Seq(t[f], й0щ) состоит из одного элемента t₁[f], представляющего собой незамкнутую нормальную форму.
t[f]й0щ є (lx. if Zero x then fx⁺ else W)й0щ ®® f й1щ є t₁[f] О NF\NF⁰.
t₁[t[f]] є (lx. if Zero x then fx⁺ else W)й1щ ®® W, следовательно, терм t₁[t[f]] не имеет нормальной формы. Согласно теореме 1, не имеет нормальной формы и терм tй0щ, так как для любого n > 1   tⁿ[f]й0щ = W.
   Рассмотрим уравнение
   f = lx. if Zero x then fx⁺ else (if Zero  x^- then (fx⁺)W else lx.I) є t[f],
где x,f О V.
Покажем, что последовательность Seq(t[f], й0щ) состоит из одного элемента t₁[f], представляющего собой незамкнутую нормальную форму.
t[f]й0щ є (lx. if Zero x then fx⁺ else (if Zero x^- then (fx⁺)W else lx.I))й0щ ®® f й1щW є t₁[f] О NF\NF⁰.
t₁[t[f]] є (lx. if Zero x then fx⁺ else (if Zero x^- then (fx⁺)W else lx.I))й1щ ®®  fй2щW, следовательно, терм t₁[t[f]] не имеет нормальной формы. Однако, согласно теореме 1, tй0щ ®® I, так как t³[f]й0щ ®® I.
   Теорема 4 доказана.
   Теорема 5. Пусть дано уравнение (1), его решение (2) и термы t₀,n₁,n₂,ј,n_k О NF⁰, где k і 0. Пусть tў - некоторое решение уравнения (1). Тогда: tn₁n₂јn_k ®® t₀ Ю  tўn₁n₂јn_k ®® t₀.
   Доказательство. Пусть tn₁n₂јn_k ®® t₀, тогда, согласно теореме 1, существует такое n і 1, что tⁿ[f]n₁n₂јn_k ®® t₀. Следовательно, и tⁿ[tў]n₁n₂јn_k ®® t₀. Так как tў - решение уравнения (1), то tў = tⁿ[tў], tўn₁n₂јn_k = tⁿ[tў]n₁n₂јn_k и, согласно следствию CR-теоремы, tўn₁n₂јn_k ®® t₀. Теорема 5 доказана.
   Теорема 6. Существует такое уравнение (1), такое его решение tў, и такие термы t₀,n₁,n₂,ј,n_k О NF⁰, где k і 0, что:

tўn1n2јnk ®® t0,    однако   tn1n2јnk t0.

   Доказательство. Рассмотрим уравнение f = f, где f О V, и его решение tў є lx.x. Терм t₀ є lx.x и k = 0. Очевидно, что tў®® t₀. Покажем, что терм t не имеет нормальной формы: t є Y(lf.f) є (lh.(lx.h(xx))(lx.h(xx)))(lf.f) ® (lx.(lf.f)(xx))(lx.(lf.f)(xx)) ®® (lx.xx)(lx.xx) є W. Теорема 6 доказана.

   Ереванский государственный университет
   ЕрНИИ АСУ

Литература

   1. Barendregt H.P. The Lambda Calculus, Its Syntax and Semantics. North-Holland Pub. Comp., 1981 (рус. пер. Барендрегт Х. Ламбда-исчисление, его синтаксис и семантика. М.: Мир, 1985).