Новые доказательства важных теорем бестипового экстенсионального λ–исчисления
Построены новые доказательства двух теорем бестипового экстенсионального λ-исчисления: теоремы Карри о том, что произвольный λ-терм имеет βŋ-нормальную форму тогда и только тогда, когда он имеет β-нормальную форму, и теоремы нормализации для βŋ-редукции. Приведенный подход базируется на двух широко...
Gespeichert in:
| Datum: | 2014 |
|---|---|
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russian |
| Veröffentlicht: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2014
|
| Schriftenreihe: | Кибернетика и системный анализ |
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/115820 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Новые доказательства важных теорем бестипового экстенсионального λ–исчисления / А.А. Лялецкий // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 53-63. — Бібліогр.: 5 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-115820 |
|---|---|
| record_format |
dspace |
| spelling |
nasplib_isofts_kiev_ua-123456789-1158202025-06-03T16:25:10Z Новые доказательства важных теорем бестипового экстенсионального λ–исчисления Нові доведення важливих теорем безтипового екстенсіонального λ-числення New proofs of important theorems of untyped extensional λ-calculus Лялецкий, А.А. Кибернетика Построены новые доказательства двух теорем бестипового экстенсионального λ-исчисления: теоремы Карри о том, что произвольный λ-терм имеет βŋ-нормальную форму тогда и только тогда, когда он имеет β-нормальную форму, и теоремы нормализации для βŋ-редукции. Приведенный подход базируется на двух широко известных результатах: теореме об откладывании ŋ-редукции и свойстве сильной нормализуемости ŋ-редукции, которые позволяют естественным образом распространить некоторые утверждения с обычного λ-исчисления на экстенсиональный случай. Наведено нові доведення двох теорем безтипового екстенсіонального λ-числення: теореми Каррі про те, що будь-який λ-терм має βŋ-нормальну форму тоді й тільки тоді, коли він має β-нормальну форму, та теореми нормалізації для βŋ-редукції. Даний підхід грунтується на двох широко відомих результатах: теоремі про відкладання ŋ-редукції та властивості сильної нормалізовності ŋ-редукції, які дозволяють природним чином розповсюдити деякі твердження зі звичайного λ-числення на екстенсіональний випадок. The paper contains new proofs of the following two theorems for the untyped extensional λ-calculus: the Curry theorem that any λ-term has a βŋ-normal form if and only if it has a β-normal form, and the normalization theorem for βŋ-reduction. Our approach is based on the following well-known results: the postponement theorem of ŋ-reduction and the strong normalization property of ŋ-reduction, which allow one to extend, in a natural way, some propositions from the usual λ-calculus onto the extensional case. 2014 Article Новые доказательства важных теорем бестипового экстенсионального λ–исчисления / А.А. Лялецкий // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 53-63. — Бібліогр.: 5 назв. — рос. https://nasplib.isofts.kiev.ua/handle/123456789/115820 510.584 ru Кибернетика и системный анализ application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Russian |
| topic |
Кибернетика Кибернетика |
| spellingShingle |
Кибернетика Кибернетика Лялецкий, А.А. Новые доказательства важных теорем бестипового экстенсионального λ–исчисления Кибернетика и системный анализ |
| description |
Построены новые доказательства двух теорем бестипового экстенсионального λ-исчисления: теоремы Карри о том, что произвольный λ-терм имеет βŋ-нормальную форму тогда и только тогда, когда он имеет β-нормальную форму, и теоремы нормализации для βŋ-редукции. Приведенный подход базируется на двух широко известных результатах: теореме об откладывании ŋ-редукции и свойстве сильной нормализуемости ŋ-редукции, которые позволяют естественным образом распространить некоторые утверждения с обычного λ-исчисления на экстенсиональный случай. |
| format |
Article |
| author |
Лялецкий, А.А. |
| author_facet |
Лялецкий, А.А. |
| author_sort |
Лялецкий, А.А. |
| title |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| title_short |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| title_full |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| title_fullStr |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| title_full_unstemmed |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| title_sort |
новые доказательства важных теорем бестипового экстенсионального λ–исчисления |
| publisher |
Інститут кібернетики ім. В.М. Глушкова НАН України |
| publishDate |
2014 |
| topic_facet |
Кибернетика |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/115820 |
| citation_txt |
Новые доказательства важных теорем бестипового экстенсионального λ–исчисления / А.А. Лялецкий // Кибернетика и системный анализ. — 2014. — Т. 50, № 4. — С. 53-63. — Бібліогр.: 5 назв. — рос. |
| series |
Кибернетика и системный анализ |
| work_keys_str_mv |
AT lâleckijaa novyedokazatelʹstvavažnyhteorembestipovogoékstensionalʹnogolisčisleniâ AT lâleckijaa novídovedennâvažlivihteorembeztipovogoekstensíonalʹnogolčislennâ AT lâleckijaa newproofsofimportanttheoremsofuntypedextensionallcalculus |
| first_indexed |
2025-11-24T14:40:58Z |
| last_indexed |
2025-11-24T14:40:58Z |
| _version_ |
1849683092067844096 |
| fulltext |
ÓÄÊ 510.584
À.À. ËßËÅÖÊÈÉ
ÍÎÂÛÅ ÄÎÊÀÇÀÒÅËÜÑÒÂÀ ÂÀÆÍÛÕ ÒÅÎÐÅÌ ÁÅÑÒÈÏÎÂÎÃÎ
ÝÊÑÒÅÍÑÈÎÍÀËÜÍÎÃÎ �-ÈÑ×ÈÑËÅÍÈß
Àííîòàöèÿ. Ïîñòðîåíû íîâûå äîêàçàòåëüñòâà äâóõ òåîðåì áåñòèïîâîãî ýêñòåíñèîíàëüíî-
ãî �-èñ÷èñëåíèÿ: òåîðåìû Êàððè î òîì, ÷òî ïðîèçâîëüíûé �-òåðì èìååò ��-íîðìàëüíóþ
ôîðìó òîãäà è òîëüêî òîãäà, êîãäà îí èìååò �-íîðìàëüíóþ ôîðìó, è òåîðåìû íîðìàëèçà-
öèè äëÿ ��-ðåäóêöèè. Ïðèâåäåííûé ïîäõîä áàçèðóåòñÿ íà äâóõ øèðîêî èçâåñòíûõ ðå-
çóëüòàòàõ: òåîðåìå îá îòêëàäûâàíèè �-ðåäóêöèè è ñâîéñòâå ñèëüíîé íîðìàëèçóåìîñòè
�-ðåäóêöèè, êîòîðûå ïîçâîëÿþò åñòåñòâåííûì îáðàçîì ðàñïðîñòðàíèòü íåêîòîðûå óòâåð-
æäåíèÿ ñ îáû÷íîãî �-èñ÷èñëåíèÿ íà ýêñòåíñèîíàëüíûé ñëó÷àé.
Êëþ÷åâûå ñëîâà: áåñòèïîâîå ýêñòåíñèîíàëüíîå �-èñ÷èñëåíèå, îòêëàäûâàíèå �-ðåäóêöèè,
òåîðåìà î ��-íîðìàëüíîé ôîðìå, òåîðåìà íîðìàëèçàöèè äëÿ ��-ðåäóêöèè.
 íàñòîÿùåé ñòàòüå ïðèâåäåíû íîâûå ïðîñòûå äîêàçàòåëüñòâà äâóõ âàæíûõ ðå-
çóëüòàòîâ áåñòèïîâîãî ýêñòåíñèîíàëüíîãî �-èñ÷èñëåíèÿ: òåîðåìû Êàððè î òîì,
÷òî ïðîèçâîëüíûé �-òåðì èìååò ��-íîðìàëüíóþ ôîðìó òîãäà è òîëüêî òîãäà,
êîãäà îí èìååò �-íîðìàëüíóþ ôîðìó, è òåîðåìû íîðìàëèçàöèè äëÿ ��-ðåäóêöèè.
Èñïîëüçóåìûé ïîäõîä áàçèðóåòñÿ íà äâóõ øèðîêî èçâåñòíûõ ðåçóëüòàòàõ: òåîðå-
ìå îá îòêëàäûâàíèè �-ðåäóêöèè è î÷åâèäíîì ñâîéñòâå ñèëüíîé íîðìàëèçóåìîñòè
�-ðåäóêöèè, êîòîðûå, êàê áóäåò âèäíî äàëåå, ïîçâîëÿò åñòåñòâåííûì îáðàçîì ðàñ-
ïðîñòðàíèòü íåêîòîðûå óòâåðæäåíèÿ ñ îáû÷íîãî �-èñ÷èñëåíèÿ íà ýêñòåíñèîíàëü-
íûé ñëó÷àé. Ïðè ýòîì òåîðåìà îá îòêëàäûâàíèè �-ðåäóêöèè äîïóñêàåò ýëåìåí-
òàðíîå äîêàçàòåëüñòâî, íå èñïîëüçóþùåå íèêàêèõ ñïåöèàëüíûõ çíàíèé íè î �-ðå-
äóêöèè, íè îá �-ðåäóêöèè, êîòîðîå òàêæå ïðèâåäåíî â äàííîé ðàáîòå.
Îòìåòèì, ÷òî â ðàáîòàõ î �-èñ÷èñëåíèè [1–3] ðàññìîòðåíû äîâîëüíî äëèí-
íûå è òåõíè÷åñêè ñëîæíûå äîêàçàòåëüñòâà óêàçàííûõ ðåçóëüòàòîâ, îäíàêî èõ
ïðåèìóùåñòâî — êîíñòðóêòèâíîñòü. Â íàñòîÿùåé ñòàòüå ñòðîÿòñÿ áîëåå êîðîò-
êèå è ëîãè÷åñêè áîëåå ïðîçðà÷íûå äîêàçàòåëüñòâà, ïðè÷åì ñ ïîìîùüþ òîëüêî
ýëåìåíòàðíûõ ìåòîäîâ �-èñ÷èñëåíèÿ.
Èñïîëüçóåì äàëåå òåðìèíîëîãèþ èç [1]. Ïðè ðàññìîòðåíèè �-òåðìîâ âñþäó
ïðåäïîëàãàåì, ÷òî âûïîëíåíî ñîãëàøåíèå îá óïîòðåáëåíèè ïåðåìåííûõ. Ó÷èòû-
âàÿ îáùóþ íàïðàâëåííîñòü äàííîé ðàáîòû è æåëàÿ ñäåëàòü åå ñîäåðæàíèå ñàìî-
äîñòàòî÷íûì ñ òî÷êè çðåíèÿ ýêñòåíñèîíàëüíîãî �-èñ÷èñëåíèÿ, áóäåì ïðèâîäèòü
íåîáõîäèìûå îïðåäåëåíèÿ, à òàêæå ôîðìóëèðîâêè è äîêàçàòåëüñòâà ðåçóëüòàòîâ,
èìåþùèõ îòíîøåíèå ê ��-ðåäóêöèè è ��-êîíâåðñèè è èñïîëüçóþùèõñÿ ïðè ïî-
ëó÷åíèè îñíîâíûõ ðåçóëüòàòîâ; ÷òî êàñàåòñÿ �-ðåäóêöèè è �-êîíâåðñèè, îãðàíè-
÷èìñÿ ññûëêàìè íà ëèòåðàòóðó.
Äàëåå �-òåðìû áóäåì îáîçíà÷àòü ñèìâîëàìè t , p, q , u, �, w, ïåðåìåííûå —
ñèìâîëàìè x è y , ðåäåêñû — ñèìâîëîì �, ñîâîêóïíîñòü âñåõ �-òåðìîâ è ìíîæåñ-
òâî âñåõ ïåðåìåííûõ — ñèìâîëàìè � è X ñîîòâåòñòâåííî.
Îïðåäåëåíèå 1. Ïóñòü R0 è R1 — ïðîèçâîëüíûå áèíàðíûå îòíîøåíèÿ, çà-
äàííûå íà êàêîì-òî ìíîæåñòâå A. Ãîâîðÿò, ÷òî R0 îòêëàäûâàåòñÿ îòíîñèòåëüíî
R1, åñëè âûïîëíÿåòñÿ ñëåäóþùàÿ äèàãðàììà:
(1)
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 53
R0
R1
R1
R0
© À.À. Ëÿëåöêèé, 2014
ò.å. åñëè R R R R0 1 1 0� �� , ãäå ñèìâîë � îáîçíà÷àåò îáû÷íóþ êîìïîçèöèþ áè-
íàðíûõ îòíîøåíèé.
Çàìåòèì, ÷òî åñëè îòíîøåíèÿ R0 è R1 ÿâëÿþòñÿ ôóíêöèîíàëüíûìè (ò.å.
óíàðíûìè îïåðàöèÿìè íà A), òî R0 îòêëàäûâàåòñÿ îòíîñèòåëüíî R1 òîãäà è òîëü-
êî òîãäà, êîãäà R R R R0 1 1 0� �� ; îäíàêî â îáùåì ñëó÷àå èç òîãî, ÷òî R0 îòêëà-
äûâàåòñÿ îòíîñèòåëüíî R1, íå ñëåäóåò, ÷òî R1 îòêëàäûâàåòñÿ îòíîñèòåëüíî R0 ,
â ÷åì ëåãêî óáåäèòüñÿ, ðàññìîòðåâ ïðèìåðû.
Áóäåì îáîçíà÷àòü R * ðåôëåêñèâíî-òðàíçèòèâíîå çàìûêàíèå áèíàðíîãî îò-
íîøåíèÿ R. Ñëåäóþùèå äâå ëåììû ìîæíî ðàññìàòðèâàòü êàê ïðîòîòèïû ðàçëè÷-
íûõ òåîðåì îá îòêëàäûâàíèè.
Ëåììà 1. Ïóñòü R0 è R1 — áèíàðíûå îòíîøåíèÿ, çàäàííûå íà êàêîì-òî
ìíîæåñòâå A, ïðè÷åì R0 îòêëàäûâàåòñÿ îòíîñèòåëüíî R1. Òîãäà
( ) ( ) ( )* * *R R R R0 1 1 0� �� .
Äîêàçàòåëüñòâî. Î÷åâèäíî, ÷òî ( ) ( ) ( )* * *R R R R0 1 1 0� �� . Äîêàæåì ïðî-
òèâîïîëîæíîå âêëþ÷åíèå. Ïðåäïîëîæèì, ÷òî äëÿ íåêîòîðûõ ýëåìåíòîâ a è b
ìíîæåñòâà A èìååò ìåñòî îòíîøåíèå a R R b( )*
0 1� . Ïðè ýòîì áåç óìàëåíèÿ îáù-
íîñòè ìîæíî ñ÷èòàòü, ÷òî a b� .  ýòîì ñëó÷àå ñóùåñòâóåò êîíå÷íàÿ ïîñëåäîâà-
òåëüíîñòü ýëåìåíòîâ ìíîæåñòâà A âèäà
a a R R a R R R R a bn� � � 0 0 1 1 0 1 0 1 1( ) ( ) ( )� � � ,
ò.å. ëþáàÿ ïàðà ai è ai
1 ñîñåäíèõ ýëåìåíòîâ ýòîé ïîñëåäîâàòåëüíîñòè íàõî-
äèòñÿ â îòíîøåíèè R0 èëè â îòíîøåíèè R1. Åñëè âñå ïàðû ñîñåäíèõ ýëåìåí-
òîâ íàõîäÿòñÿ ëèáî îäíîâðåìåííî â îòíîøåíèè R0 , ëèáî îäíîâðåìåííî â îò-
íîøåíèè R1, òî óòâåðæäåíèå ëåììû î÷åâèäíî.  ïðîòèâíîì ñëó÷àå ñóùåñòâó-
åò òàêîå íàèáîëüøåå ÷èñëî i, 0 3� � i n , ÷òî âûïîëíÿþòñÿ ñîîòíîøåíèÿ
a R a R ai i a0 1 1 2
, ò.å. äàííàÿ ïîñëåäîâàòåëüíîñòü èìååò âèä
a R R a R R R R a R a R a R R a Ri i i i k0 0 1 1 0 1 0 1 0 1 1 2 1 1( ) ( ) ( )� � � � �
1 1 1� R an .
 ñèëó (1) ñóùåñòâóåò òàêîé ýëåìåíò ci
1, ÷òî a R c R ai i a1 1 0 2
, è ìîæíî
ïðèâåñòè ïîñëåäíþþ ïîñëåäîâàòåëüíîñòü ê âèäó
a R R a R R R R a R ñ R a R R ai i i i k0 0 1 1 0 1 0 1 1 1 0 2 1 1( ) ( ) ( )� � � � �
1 0 0 1R R an� .
Ïîâòîðèâ ýòî äåéñòâèå k 2 ðàç, ïðèõîäèì ê ïîñëåäîâàòåëüíîñòè
a R R a R R R R a R ñ R ñ R R ñi i i i k0 0 1 1 0 1 0 1 1 1 0 2 0 0( ) ( ) ( )� � � � �
1 0 0 1R R an� .
Äâà ïîñëåäíèõ ÷ëåíà ýòîé ïîñëåäîâàòåëüíîñòè óäîâëåòâîðÿþò ñîîòíîøåíèþ
ñ R an n 2 0 1, è ìîæíî ïðèìåíèòü èíäóêöèþ ïî äëèíå ïîñëåäîâàòåëüíîñòè.
Ëåììà äîêàçàíà.
Îïðåäåëåíèå 2. Ïóñòü R0 è R1 — áèíàðíûå îòíîøåíèÿ, çàäàííûå íà êà-
êîì-òî ìíîæåñòâå A. Ãîâîðÿò, ÷òî R0 îòêëàäûâàåòñÿ îòíîñèòåëüíî R1 â îñëàá-
ëåííîì ñìûñëå, èëè ÷òî R0 ñëàáî îòêëàäûâàåòñÿ îòíîñèòåëüíî R1, åñëè èìååò
ìåñòî äèàãðàììà
(2)
54 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
R0
R1
R1
*
R0
*
Ëåììà 2. Ïóñòü R0 è R1 — áèíàðíûå îòíîøåíèÿ, çàäàííûå íà êàêîì-òî
ìíîæåñòâå A. Òîãäà:
1) äëÿ òîãî ÷òîáû R0
* îòêëàäûâàëîñü îòíîñèòåëüíî R1
* , íåîáõîäèìî è äîñòà-
òî÷íî, ÷òîáû R0 ñëàáî îòêëàäûâàëîñü îòíîñèòåëüíî R1;
2) åñëè R0
* îòêëàäûâàåòñÿ îòíîñèòåëüíî R1
* , òî ( )* * * * *R R R R0 1 1 0� �� .
Äîêàçàòåëüñòâî. 1. Íåîáõîäèìîñòü î÷åâèäíà. Äîêàæåì äîñòàòî÷íîñòü. Âíà-
÷àëå èç äèàãðàììû (2) âûâåäåì äèàãðàììó
(3)
Äåéñòâèòåëüíî, îíà ñëåäóåò èç äèàãðàììû
Àíàëîãè÷íî, èç äèàãðàììû (3) ñëåäóåò äèàãðàììà
êîòîðàÿ, â ñâîþ î÷åðåäü, äîêàçûâàåò, ÷òî ñïðàâåäëèâà äèàãðàììà
ò.å. R0
* äåéñòâèòåëüíî ïåðåñòàíîâî÷íî ñ R1
* .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 55
R1
R1
R0
*
R0
*
R0
R1
R1
R0
R0
R0
R1
R1R0
R0
R1
R1
R1
R1
R1
R1
R1
R0
*
R0
*
R0
*
R0
*
R0
*
R0
*
R0
*
R1
*
R1
*
2. Åñëè R0
* ïåðåñòàíîâî÷íî ñ R1
* , òî â ñèëó ëåììû 1 èìååì
( ) (( ) ( ))* * * * * * * * *R R R R R R0 1 1 0 1 0� � �� � .
Ëåììà äîêàçàíà.
Ïðèâåäåì ñëåäóþùèå îïðåäåëåíèÿ.
Îïðåäåëåíèå 3. Ïîíÿòèå ðåäóêöèè R — ýòî ïðîèçâîëüíîå áèíàðíîå îòíîøå-
íèå íà ìíîæåñòâå � âñåõ �-òåðìîâ. Êàæäîå ïîíÿòèå ðåäóêöèè R ïîðîæäàåò îòíîøå-
íèå �R îäíîøàãîâîé R-ðåäóêöèè êàê ñîâìåñòèìîå (ñ ñèìâîëè÷åñêèìè îïåðàöèÿìè
�-èñ÷èñëåíèÿ) çàìûêàíèå R, îòíîøåíèå �R ìíîãîøàãîâîé R-ðåäóêöèè — êàê
ðåôëåêñèâíî-òðàíçèòèâíîå çàìûêàíèå �R è îòíîøåíèå �R R-êîíâåðñèè —
êàê ýêâèâàëåíòíîå çàìûêàíèå �R . Åñëè äëÿ êàêèõ-òî äâóõ �-òåðìîâ: � è
� , èìå-
åò ìåñòî �
� �� �, R, òî � íàçûâàåòñÿ R-ðåäåêñîì, à
� — åãî ñâåðòêîé (â îáùåì
ñëó÷àå R-ðåäåêñ ìîæåò èìåòü íåñêîëüêî ñâåðòîê).
Ñëåäîâàòåëüíî, u R� � èìååò ìåñòî òîãäà è òîëüêî òîãäà, êîãäà u C� [ ]�
è � �
C [ ]� äëÿ íåêîòîðîãî R-êîíòåêñòà C [ ] ñ îäíîé äûðîé, ãäå � ÿâëÿåòñÿ
R-ðåäåêñîì è
� — åãî ñâåðòêîé.
Äëÿ ëþáîãî ïîíÿòèÿ ðåäóêöèè R îáû÷íûì îáðàçîì îïðåäåëÿþòñÿ òàê íàçû-
âàåìûå R-ðåäóêöèîííûå öåïî÷êè è ñòðîÿòñÿ R-ðåäóêöèîííûå ãðàôû Gr tR ( ) äëÿ
ëþáîãî �-òåðìà t.
Îïðåäåëåíèå 4. Ïîíÿòèå �-ðåäóêöè ââîäèòñÿ êàê áèíàðíîå îòíîøåíèå
� �� � � �{ . , | }x wx w x w , ïîíÿòèå ��-ðåäóêöèè — ðàâåíñòâîì �� � �� � .
Ýòè ïîíÿòèÿ ðåäóêöèè îïèñàííûì âûøå ñïîñîáîì èíäóöèðóþò ñîîòâåòñòâó-
þùèå îòíîøåíèÿ îäíîøàãîâîé è ìíîãîøàãîâîé ðåäóêöèé, ñîîòâåòñòâóþùèå îò-
íîøåíèÿ êîíâåðñèè è ïðî÷èå �- è ��-òåðìèíû. Ýêñòåíñèîíàëüíîå �-èñ÷èñëåíèå
èçó÷àåò, â îñíîâíîì, ñâîéñòâà îòíîøåíèé ��� è � �� . Çàìåòèì, ÷òî ïîíÿòèå
��-ðåäóêöèè óñòðîåíî òàêèì îáðàçîì, ÷òî ñâåðòêà
� ëþáîãî ��-ðåäåêñà � îäíî-
çíà÷íî îïðåäåëÿåòñÿ ïî � (íî îáðàòíîå íå âåðíî).
Ïîñêîëüêó ëþáîå ïðèìåíåíèå îäíîøàãîâîé �-ðåäóêöèè óìåíüøàåò äëèíó
òåðìà, ïîíÿòèå �-ðåäóêöèè ñèëüíî íîðìàëèçóåìî, ò.å. íå ñóùåñòâóåò áåñêîíå÷-
íûõ �-ðåäóêöèîííûõ öåïî÷åê. Ñëåäîâàòåëüíî, ëþáîé �-òåðì èìååò �-íîðìàëü-
íóþ ôîðìó, à èç òåîðåìû ×åð÷à–Ðîññåðà äëÿ �-ðåäóêöèè (ñì. [1, c. 76–77]) ñëåäó-
åò, ÷òî òàêàÿ �-íîðìàëüíàÿ ôîðìà åäèíñòâåííà. Îäíàêî ïîíÿòèå �-ðåäóêöèè è,
ñëåäîâàòåëüíî, ïîíÿòèå ��-ðåäóêöèè íå ÿâëÿþòñÿ ñèëüíî íîðìàëèçóåìûìè.
Êàððè â [2] âïåðâûå ïîëó÷èë cëåäóþùèé ðåçóëüòàò äëÿ ïîñòðîåíèÿ ïåðâîãî
äîêàçàòåëüñòâà òåîðåìû ×åð÷à–Ðîññåðà äëÿ ��-ðåäóêöèè. Ïðèâåäåííîå äàëåå äî-
êàçàòåëüñòâî áëèçêî ê îðèãèíàëüíîìó äîêàçàòåëüñòâó Êàððè (äðóãîå äîêàçàòåëü-
ñòâî ñì. â [1, c. 384–387]).
Òåîðåìà îá îòêëàäûâàíèè �-ðåäóêöèè. Åñëè u��� �, òî ñóùåñòâóåò òà-
êîé �-òåðì t, ÷òî u t� �� � � .
Äîêàçàòåëüñòâî.  ñèëó ëåììû 2 äîñòàòî÷íî äîêàçàòü ÷àñòíûé ñëó÷àé îá-
ùåãî óòâåðæäåíèÿ òåîðåìû, êîòîðûé âûðàæàåòñÿ äèàãðàììîé
56 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
u
�
�
�
�
�
tt
Èíûìè ñëîâàìè, äëÿ êàæäîé äâóõøàãîâîé ðåäóêöèîííîé öåïî÷êè âèäà
u t� �
� �� �
� � �, ãäå � � è � � ÿâëÿþòñÿ âõîæäåíèÿìè �-ðåäåêñà è �-ðåäåêñà ñî-
îòâåòñòâåííî, äîñòàòî÷íî ïîñòðîèòü òàêîé �-òåðì t, ÷òî u t� �� � �. Ïóñòü
� � �� x wx. è � � �� ( . )y p q. Ñëåäîâàòåëüíî, ñâåðòêà �-ðåäåêñà � � ðàâíà w. Ðàñ-
ñìîòðèì âîçìîæíûå ñëó÷àè âçàèìíîãî ðàñïîëîæåíèÿ � � è w â �-òåðìå
t :
Ëåãêî çàìåòèòü, ÷òî â ñëó÷àÿõ 1 è 2, à òàêæå ïîäñëó÷àå 3.1 ñóùåñòâóåò åäèíñò-
âåííîå âõîæäåíèå �-ðåäåêñà �
�
� â u, êîòîðîå ïåðåõîäèò â � � ïðè îñóùåñòâëåíèè
îäíîøàãîâîé �-ðåäóêöèè u t�
� �
� . Òåïåðü î÷åâèäíî, ÷òî åñëè íà÷àòü ñ �-òåðìà
u è ïîìåíÿòü ïîðÿäîê ñâîðà÷èâàíèÿ ðåäåêñîâ � � è � � (ò.å. åñëè âíà÷àëå ñâåðíóòü
�
�
� , à çàòåì — îñòàâøååñÿ îò � �), òî ðåçóëüòèðóþùèé òåðì íå èçìåíèòñÿ.
 ïîäñëó÷àå 3.2 �-òåðì u èìååò âèä u C x y p x q� [( .( . ) ) ]� � äëÿ ïîäõîäÿùåãî
êîíòåêñòà C [ ] ñ îäíîé äûðîé. Èìååì
ïîñêîëüêó ( . ) ( . [ : ])� �y p q x p y x q� � .
 ïîäñëó÷àå 3.3 �-òåðì q ìîæíî ïðåäñòàâèòü â âèäå q Cq�
[ ]� � ,
à �-òåðì u — â âèäå u C y y y Cq� [( . ) [ ]]� �� � � � , ãäå Cq [ ] è C[ ] — ïîäõîäÿ-
ùèå êîíòåêñòû ñ îäíîé äûðîé è �y y y p.� � � � . Ïîëó÷àåì
Òåîðåìà äîêàçàíà.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 57
1. � � � w � �
2. � � � w
3. w � � �
3.1. w p�
3.2. w y p� � .
3.3. w q�
C x y p x q[( .( . ) ) ]� �
C p y q[ [ : ]]�
�
� �
�
( . )�y p x
( . )�y p q
� �x y p x. ( . )
��x p y x q. [ : ])�
C x p y x q[( . [ : ]) ]� � C y p q[( . ) ]�
C y y y Cq[( . ) [ ]]� �� � � �
C C w C wq q[( [ ] [ ] )]� � �
�
� �
�
( . )�y p x
( . ) [ ]�y y y C wq� � �
��
C C Cq q[( [ ] [ ] )]� � �� �� � C y y y Cq h[( . ) [ ]]� � � � �
Äîêàæåì óïîìÿíóòóþ ðàíåå òåîðåìó Êàððè î òîì, ÷òî íàëè÷èå ó ïðîèçâîëü-
íîãî �-òåðìà ��-íîðìàëüíîé ôîðìû ðàâíîñèëüíî íàëè÷èþ ó íåãî �-íîðìàëüíîé
ôîðìû. Âïåðâûå ýòó òåîðåìó ïîëó÷èë Êàððè â [3] ñ ïîìîùüþ ïðÿìîãî äîêàçàòåëü-
ñòâà, ïîäîáíîãî ïðèâåäåííîìó âûøå äîêàçàòåëüñòâó òåîðåìû îá îòêëàäûâàíèè
�-ðåäóêöèè. Äðóãîå äîêàçàòåëüñòâî ïîëó÷èë Õ. Áàðåíäåðãò è äð. â [4] (ñì. òàêæå
[1, ñ. 384–386]). Õîä ïðèâåäåííîãî äàëåå äîêàçàòåëüñòâà â öåëîì ñëåäóåò äîêàçà-
òåëüñòâó Êàððè, íî áàçèðóåòñÿ íà îäíîì ñïåöèàëüíîì ôîðìàëèçìå èç [1, 4], ïî-
çâîëÿþùåì ñóùåñòâåííî óïðîñòèòü ëîãè÷åñêèå ïîñòðîåíèÿ è âû÷èñëåíèÿ.
Òåîðåìà î ��-íîðìàëüíîé ôîðìå. Ïðîèçâîëüíûé �-òåðì èìååò ��-íîð-
ìàëüíóþ ôîðìó òîãäà è òîëüêî òîãäà, êîãäà îí èìååò �-íîðìàëüíóþ ôîðìó.
Äîêàçàòåëüñòâî. Äîñòàòî÷íîñòü. Äåéñòâèòåëüíî, åñëè �-òåðì t èìååò �-íîð-
ìàëüíóþ ôîðìó, ñêàæåì,
t , òî ïðèìåíåíèÿ �-ðåäóêöèè ê âõîæäåíèÿì �-ðåäåêñîâ
â
t óìåíüøàþò äëèíó
t è íå ñîçäàþò íîâûõ �-ðåäåêñîâ.
Íåîáõîäèìîñòü.  ñèëó òåîðåìû îá îòêëàäûâàíèè �-ðåäóêöèè, äîñòàòî÷íî
óñòàíîâèòü ñëåäóþùåå óòâåðæäåíèå.
Óòâåðæäåíèå 1. Åñëè t t��
è
t ÿâëÿåòñÿ �-íîðìàëüíîé ôîðìîé, òî t èìååò
�-íîðìàëüíóþ ôîðìó.
Äëÿ òîãî ÷òîáû óäîñòîâåðèòüñÿ â ñïðàâåäëèâîñòè óòâåðæäåíèÿ 1, âíà÷àëå
ââåäåì âñïîìîãàòåëüíîå ðàñøèðåíèå �� ÿçûêà � , ýëåìåíòû êîòîðîãî íàçûâàþò-
ñÿ ��-òåðìàìè.
Îïðåäåëåíèå 5. Ãðóáî ãîâîðÿ, ��-òåðì — ýòî ïðîèçâîëüíûé �-òåðì, íåêîòî-
ðûå (íàïðèìåð, âñå èëè íèêàêèå) âõîæäåíèÿ ïîäòåðìîâ â êîòîðûé ïîìå÷åíû îä-
íîé èëè íåñêîëüêèìè �-ìåòêàìè. Áîëåå ôîðìàëüíî ÿçûê �� îïðåäåëÿåòñÿ êàê íà-
èìåíüøåå ìíîæåñòâî ñëîâ â àëôàâèòå ÿçûêà îáû÷íûõ �-òåðìîâ, äîïîëíåííîì
ñïåöèàëüíûì ñèìâîëîì �, óäîâëåòâîðÿþùåå ñëåäóþùèì óñëîâèÿì:
� x — ïåðåìåííàÿ � ñëîâî x ��� ;
� t0 , t t t1 0 1� � �� �� � ;
� x — ïåðåìåííàÿ è t ��� � � �
x t. �� ;
� t t� � �� �� � � .
Èòàê, ��-òåðì — ýòî ñëîâî ÿçûêà �� .
Ââåäåì â ðàññìîòðåíèå ñëåäóþùèå äâà îòîáðàæåíèÿ: | | è �.
Îòîáðàæåíèå | | : � �� � ñòèðàåò âñå �-ìåòêè â ëþáîì ��-òåðìå (íèêàê áî-
ëåå íå èçìåíÿÿ åãî), à îòîáðàæåíèå � �: � �� îïðåäåëÿåòñÿ èíäóêöèåé ïî ïî-
ñòðîåíèþ ��-òåðìà:
� �( ) ,x x x� — ïåðåìåííàÿ;
� � � �( ) ( ) ( )t t t t0 1 0 1� ;
� � � � �( . ) . ( )x t x t� ;
� � � ��( ) . ( ) ,t y t y y� — íîâàÿ ïåðåìåííàÿ.
Èíûìè ñëîâàìè, îòîáðàæåíèå � â êàæäîì ��-òåðìå «ðàçâîðà÷èâàåò» âñå åãî
�-ìàðêèðîâàííûå ïîäòåðìû, íà÷èíàÿ èçíóòðè. Çàìåòèì, ÷òî èç îïðåäåëåíèé íå-
ïîñðåäñòâåííî ñëåäóåò (èíäóêöèåé ïî ïîñòðîåíèþ ��-òåðìà), ÷òî âñåãäà
� �( ) | |t t� . Â êîíòåêñòå äàííîãî äîêàçàòåëüñòâà îòîáðàæåíèÿ | | è � áûëè ââåäå-
íû äëÿ òîãî, ÷òîáû ñôîðìóëèðîâàòü ñëåäóþùåå óòâåðæäåíèå: åñëè
t ÿâëÿåòñÿ
�-íîðìàëüíîé ôîðìîé �-òåðìà t , òî ñóùåñòâóåò òàêîé (åäèíñòâåííûé) ��-òåðì
~
t ,
÷òî |
~
|
�
t t è �(
~
)
�t t . Ïîýòîìó óòâåðæäåíèå 1 ëîãè÷åñêè ýêâèâàëåíòíî ñëåäóþ-
ùåìó óòâåðæäåíèþ, çàèìñòâîâàííîìó èç [1, ñ. 385–386, 4]).
58 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
Ëåììà Áàðåíäðåãòà. Ïóñòü t — ïðîèçâîëüíûé ��-òåðì. Åñëè | |t ÿâëÿåòñÿ
�-íîðìàëüíîé ôîðìîé, òî �( )t èìååò �-íîðìàëüíóþ ôîðìó ïðè ëþáîì ��-òåðìå t.
Ïðåæäå, ÷åì ïðèñòóïèòü ê äîêàçàòåëüñòâó ýòîé ëåììû, óñòàíîâèì âñïîìîãà-
òåëüíûå ñâîéñòâà îòîáðàæåíèÿ �, êàñàþùèåñÿ îòíîøåíèÿ � � �-êîíâåðñèè.
Ïîäëåììà. Äëÿ ïðîèçâîëüíûõ ��-òåðìîâ u è � âûïîëíÿþòñÿ ñëåäóþùèå ñî-
îòíîøåíèÿ:
à) � ���
�
�( ) ( )u u� ;
á) � � � � � ��
�( . ) ( . ) . ( )x u x u x u� � ;
â) � � � � � � ��
�( ) ( ) ( ) ( )u u u� � .
Äîêàçàòåëüñòâî (ïîäëåììû). Ñïðàâåäëèâû ñëåäóþùèå ðàâåíñòâà:
à) � � � � � � � � ��� �
�
�( ) . ( ) .( . ( ) ) . ( ) ( )u y u y y z u z y z u z u� � � � ;
á) � � � � � � � � � � � ��
�( . ) ( .( . ) ) . ( . ( )) . ( ) (x u y x u y y x u y y u x� � � � . )u ;
â) � � � � � � � � � � ��
�( ) ( . ( ) ) ( ) ( ) ( ) ( )u y u y u u� � � .
Äîêàçàòåëüñòâî ëåììû Áàðåíäðåãòà ïðîâåäåì èíäóêöèåé ïî ïîñòðîåíèþ
�-òåðìà | |t .
Ñëó÷àé 1. Òåðì | |t ÿâëÿåòñÿ ïåðåìåííîé, t x� . Ñëåäîâàòåëüíî, | | *t x� , ãäå *
îáîçíà÷àåò íóëü, îäèí èëè íåñêîëüêî ìàðêåðîâ �. Èç òîæäåñòâà a) ïîäëåììû ñëå-
äóåò, ÷òî òåðì �( )t ðàâåí ëèáî x, ëèáî �y xy. â çàâèñèìîñòè îò òîãî, èìååò ëè ïå-
ðåìåííàÿ x õîòÿ áû îäèí ìàðêåð � â òåðìå t.
Ñëó÷àé 2. Òåðì | |t èìååò âèä | | .t x u� � , ãäå u íàõîäèòñÿ â �-íîðìàëüíîé ôîð-
ìå. Òîãäà t ìîæíî ïðåäñòàâèòü â âèäå t x t�
( . )*� , ãäå | |
�t u . Èç òîæäåñòâ à) è á)
ïîäëåììû âûòåêàåò, ÷òî òåðì �( )t ðàâåí � �x t. ( )
, è äîêàçûâàåìîå óòâåðæäåíèå
ñëåäóåò èç ïðåäïîëîæåíèÿ èíäóêöèè.
Ñëó÷àé 3. Òåðì | |t èìååò âèä | |t xu u uk� 1 2� , ãäå âñå �-òåðìû ui íàõîäÿòñÿ
â �-íîðìàëüíîé ôîðìå. Ñëåäîâàòåëüíî, òåðì t ìîæíî ïðåäñòàâèòü â âèäå
t x t t t
k
� (( (( ) ) ) )* * * * *
� �
1 2
, ãäå | |t ui i� . Èç ðàâåíñòâ a) è â) ïîäëåììû ñëåäó-
åò, ÷òî �( )t ðàâåí ëèáî x u u uk� � �( ) ( ) ( )1 2 � , ëèáî � � � �y x u u u yk. ( ) ( ) ( )1 2 �
â çàâèñèìîñòè îò òîãî, èìååò ëè òåðì t õîòÿ áû îäèí âíåøíèé ìàðêåð �. Òåïåðü
äîêàçûâàåìîå óòâåðæäåíèå ñëåäóåò èç ïðåäïîëîæåíèÿ èíäóêöèè.
Ýòî çàâåðøàåò äîêàçàòåëüñòâî ëåììû Áàðåíäðåãòà, à âìåñòå ñ íåé è óòâåð-
æäåíèÿ 1.
Òåîðåìà î ��-íîðìàëüíîé ôîðìå äîêàçàíà.
Ñôîðìóëèðóåì è äîêàæåì òåîðåìó íîðìàëèçàöèè äëÿ ��-ðåäóêöèè, êîòî-
ðóþ äîêàçàë ß. Êëîï â [5, c. 279–293] ñ ïîìîùüþ òàê íàçûâàåìûõ ðåäóêöèîííûõ
äèàãðàìì. Äîêàçàòåëüñòâî, ïðèâîäèìîå äàëåå, ñòðîèòñÿ íà îñíîâàíèè àíàëîãà
ýòîé òåîðåìû äëÿ �-ðåäóêöèè è äîêàçàííûõ â íàñòîÿùåé ñòàòüå ðåçóëüòàòîâ.
Îäíàêî âíà÷àëå èññëåäóåì íåêîòîðûå äîïîëíèòåëüíûå ñâîéñòâà îáùåãî ïîíÿòèÿ
ðåäóêöèè äëÿ òîãî, ÷òîáû çàòåì ïðèìåíèòü èõ ê ��-ñëó÷àþ.
Ãðóáî ãîâîðÿ, äâà �-òåðìà: t0 è t1, áóäåì ñ÷èòàòü ýêâèâàëåíòíûìè, åñëè t1
ìîæíî ïîëó÷èòü èç t0 îäíîâðåìåííûì èíúåêòèâíûì ïåðåèìåíîâàíèåì ñâîáîä-
íûõ ïåðåìåííûõ (çàìåòèì, ÷òî â ñèëó ñîãëàøåíèÿ îá óïîòðåáëåíèè ïåðåìåííûõ
ëþáûå äâà �-òåðìà òàêèå, ÷òî îäèí èç íèõ ìîæíî ïîëó÷èòü èç äðóãîãî ïåðåèìå-
íîâàíèåì ñâÿçûâàþùèõ ïåðåìåííûõ, îòîæäåñòâëÿþòñÿ). Íàïðèìåð, �-òåðìû
�a acxxyz. è �b bdyyxz. ýêâèâàëåíòíû. Áîëåå ôîðìàëüíî ýòî ïîíÿòèå ââîäèòñÿ
ñëåäóþùèì îáðàçîì.
Îïðåäåëåíèå 6. Ñèìâîëîì S X îáîçíà÷èì ãðóïïó âñåõ ïåðåñòàíîâîê ìíîæåñ-
òâà X , ãäå X — ìíîæåñòâî âñåõ ïåðåìåííûõ ÿçûêà �-òåðìîâ. Ïðîäîëæèì äåé-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 59
ñòâèå êàæäîé ïåðåñòàíîâêè � �S X äî ïåðåñòàíîâêè � èíäóêöèåé ïî ïîñòðîåíèþ
�-òåðìà
( )u u� �� � �� ; ( . ) .� �� � �x u x u� .
Íàêîíåö, �-òåðìû t0 è t1 íàçûâàþòñÿ ýêâèâàëåíòíûìè, åñëè t t1 0
� � äëÿ íåêîòîðîé
ïåðåñòàíîâêè � �S X ; ýêâèâàëåíòíîñòü �-òåðìîâ t0 è t1 áóäåì îáîçíà÷àòü t t0 1� .
Î÷åâèäíî, ÷òî � äåéñòâèòåëüíî ÿâëÿåòñÿ îòíîøåíèåì ýêâèâàëåíòíîñòè. Îáîçíà-
÷èì � s ñîâîêóïíîñòü âñåõ �-òåðìîâ, ðàçìåð êîòîðûõ ðàâåí s . Ïîñêîëüêó ïðîèçâîëü-
íûé �-òåðì ðàçìåðà s èìååò ìàêñèìóì s ðàçëè÷íûõ âõîæäåíèé ëþáûõ ïåðåìåííûõ,
ëþáîå ìíîæåñòâî ïîïàðíî íåýêâèâàëåíòíûõ �-òåðìîâ ôèêñèðîâàííîãî ðàçìåðà s ÿâ-
ëÿåòñÿ êîíå÷íûì, ò.å. äëÿ ëþáîãî s ôàêòîð-ìíîæåñòâî � s / � êîíå÷íî.
Îïðåäåëåíèå 7. Áèíàðíîå îòíîøåíèå R íà ìíîæåñòâå � íàçûâàåòñÿ àáñòðàê-
òíûì, åñëè R âûäåðæèâàåò ïðèìåíåíèå ëþáîé ïîäñòàíîâêè � �S X , ò.å. èç
� � �t t R0 1, ñëåäóåò � � �t t R
0 1
� �, .
Ïî îïðåäåëåíèþ, êàæäîå ïîíÿòèå ðåäóêöèè — ýòî áèíàðíîå îòíîøåíèå íà
ìíîæåñòâå � ; åñëè ïîíÿòèå R ðåäóêöèè ÿâëÿåòñÿ àáñòðàêòíûì, òî òàêèìè æå áóäóò
îòíîøåíèÿ îäíîøàãîâîé è ìíîãîøàãîâîé R-ðåäóêöèé, à òàêæå îòíîøåíèå R-êîí-
âåðñèè. Ïðàêòè÷åñêè âñå âàæíûå ïîíÿòèÿ ðåäóêöèè ÿâëÿþòñÿ àáñòðàêòíûìè; íàïðè-
ìåð, ïîíÿòèÿ �- è �-ðåäóêöèé è, ñëåäîâàòåëüíî, ïîíÿòèå ��-ðåäóêöèè.
Íà ñîäåðæàòåëüíîì óðîâíå ìîæíî ñêàçàòü, ÷òî ïîíÿòèå ðåäóêöèè R àáñòðàêòíî,
åñëè âñå ýêâèâàëåíòíûå ìåæäó ñîáîé �-òåðìû èìåþò ðàâíîïðàâíûå îòíîñèòåëüíî R
ñâîéñòâà.  ïðåäïîëîæåíèè àáñòðàêòíîñòè R îòñþäà âûòåêàåò, â ÷àñòíîñòè, ñëåäóþ-
ùåå. Âî-ïåðâûõ, ìíîæåñòâî R-NF âñåõ R-íîðìàëüíûõ ôîðì çàìêíóòî îòíîñèòåëüíî
îòíîøåíèÿ � : t R� -NF & t t t R�
�
� -NF. Âî-âòîðûõ, åñëè t t0 1� , ò.å. t t1 0
� � äëÿ
íåêîòîðîé ïîäñòàíîâêè � �S X , òî R-ðåäóêöèîííûå ãðàôû Gr tR ( )0 è Gr tR ( )1 �-òåð-
ìîâ t0 è t1 èçîìîðôíû, à èìåííî: Gr t Gr t Gr tR R R( ) ( ) ( )1 0 0
� �� � , ãäå îáîçíà÷åíèå
Gr t
R
� ( ) èìååò î÷åâèäíûé ñìûñë.
Îïðåäåëåíèå 8. Ïóñòü R — ïðîèçâîëüíîå ïîíÿòèå ðåäóêöèè. Íàïîìíèì, ÷òî
ïîä R-ñòðàòåãèåé ïîíèìàåòñÿ ëþáàÿ òàêàÿ ôóíêöèÿ f : � �� , ÷òî:
� t f t� ( ) , åñëè t ÿâëÿåòñÿ R-íîðìàëüíîé ôîðìîé;
� t f tR� ( ) â ïðîòèâíîì ñëó÷àå.
Êàæäóþ R-ñòðàòåãèþ f ìîæíî ðàññìàòðèâàòü êàê ÷àñòíûé ñëó÷àé ïîíÿòèÿ
ðåäóêöèè; f ÿâëÿåòñÿ àáñòðàêòíîé òîãäà è òîëüêî òîãäà, êîãäà ðàâåíñòâî
f t f t( ) ( ( ))� �� âûïîëíÿåòñÿ ïðè ëþáûõ �-òåðìå t è ïåðåñòàíîâêå � �S X . Çàìå-
òèì, ÷òî â îáùåì ñëó÷àå èç òîãî, ÷òî ïîíÿòèå R ðåäóêöèè ÿâëÿåòñÿ àáñòðàêòíûì,
íå ñëåäóåò àáñòðàêòíîñòü R-ñòðàòåãèè f , äàæå ïðè äîïîëíèòåëüíîì ïðåäïîëîæå-
íèè, î òîì, ÷òî f ÿâëÿåòñÿ îäíîøàãîâîé. Íî åñëè R ôóíêöèîíàëüíî, ò.å. åñëè
êàæäûé R-ðåäåêñ èìååò â òî÷íîñòè îäíó ñâåðòêó, òî èç àáñòðàêòíîñòè R ñëåäóåò
àáñòðàêòíîñòü âñåõ îäíîøàãîâûõ R-ñòðàòåãèé.
Îáîçíà÷èì R-NF ìíîæåñòâî âñåõ R-íîðìàëüíûõ ôîðì, R NF — ìíîæåñòâî
âñåõ �-òåðìîâ, èìåþùèõ R-íîðìàëüíóþ ôîðìó è íàêîíåö, ïîëîæèì R s
�NF
� R sNF � � .
Îïðåäåëåíèå 9. Íàïîìíèì, ÷òî R-ñòðàòåãèÿ f íàçûâàåòñÿ íîðìàëèçóþùåé,
åñëè èç òîãî, ÷òî �-òåðì t èìååò R-íîðìàëüíóþ ôîðìó, ñëåäóåò, ÷òî f t Rn ( ) � -NF
äëÿ íåêîòîðîãî íàòóðàëüíîãî ÷èñëà n .
Ëåììà 3. Ïóñòü äàíû àáñòðàêòíîå ïîíÿòèå R ðåäóêöèè è íîðìàëèçóþùàÿ
àáñòðàêòíàÿ R-ñòðàòåãèÿ f . Äëÿ ëþáîãî íàòóðàëüíîãî ÷èñëà s íàéäåòñÿ íàòóðàëü-
íîå ÷èñëî m m f s� ( , ) òàêîå, ÷òî f t Rm ( ) � -NF, åñëè òîëüêî t R s� NF .
60 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
Äîêàçàòåëüñòâî. Êàê óæå óñòàíîâëåíî, ôàêòîð-ìíîæåñòâî R s
�NF / êîíå÷-
íî. Ïðîèçâîëüíûì îáðàçîì âûáåðåì èç êàæäîãî êëàññà ýêâèâàëåíòíîñòè ïî îä-
íîìó ïðåäñòàâèòåëþ, êîòîðûå îáîçíà÷èì r r rk0 1 1, , ,� . Äëÿ ëþáîãî �-òåðìà
t R s� NF íàéäåòñÿ òàêîå ÷èñëî i, ÷òî t ri� .  ñèëó àáñòðàêòíîñòè R è f ñëåäóþ-
ùèå f -ðåäóêöèîííûå öåïî÷êè
t f t f tf f f� � �( ) ( )2
� ,
r f r f ri f i f i f� � �( ) ( )2
�
èìåþò îäèíàêîâûå àáñòðàêòíûå { , }R f -ïîðîæäåííûå ñâîéñòâà.  ÷àñòíîñòè,
åñëè mi — òàêîå íàèìåíüøåå íàòóðàëüíîå ÷èñëî, ÷òî f r R
m
i
i ( ) � -NF, òî mi
èìååò òàêîå æå ñâîéñòâî è äëÿ f -ðåäóêöèîííîé öåïî÷êè, íà÷èíàþùåéñÿ òåð-
ìîì t (òàêîå ÷èñëî mi ñóùåñòâóåò, ïîñêîëüêó t R s� NF è f — íîðìàëèçóþ-
ùàÿ ñòðàòåãèÿ). Òåïåðü, ïîëîæèâ m m
i k
i�
�
max
,0 1
, íàéäåì èñêîìîå íàòóðàëüíîå
÷èñëî m (è äàæå íàèìåíüøåå ÷èñëî, êîòîðîå èìååò íóæíîå ñâîéñòâî).
Ëåììà äîêàçàíà.
Îïðåäåëåíèå 10. Ïóñòü � 0 è � 1 — äâà âõîæäåíèÿ ��-ðåäåêñîâ â êàêîé-òî
�-òåðì t. Áóäåì ãîâîðèòü, ÷òî � 0 ðàñïîëîæåí (ñòðîãî) ëåâåå � 1 â t, è çàïèñûâàòü
� � �0 1, åñëè ëèáî ïåðâûé ñèìâîë èç � 0 ðàñïîëîæåí â t ñòðîãî ëåâåå, ÷åì ïåð-
âûé ñèìâîë èç � 1, ëèáî ðàñïîëîæåíèå ïåðâûõ ñèìâîëîâ èç � 0 è � 1 â t ñîâïàäà-
þò (à òîãäà è ñàìè ýòè ñèìâîëû ñîâïàäàþò) è ïðè ýòîì � �0 1� .
Çàìåòèì, ÷òî � �0 1� èìååò ìåñòî òîãäà è òîëüêî òîãäà, êîãäà âûïîëíÿåòñÿ
â òî÷íîñòè îäíî èç ñëåäóþùèõ óñëîâèé: ëèáî ïåðâûé ñèìâîë èç � 0 ðàñïîëîæåí â t
ñòðîãî ëåâåå, ÷åì ïåðâûé ñèìâîë èç èç � 1; ëèáî ìåñòîïîëîæåíèÿ â t ïåðâûõ ñèìâî-
ëîâ èç � 0 è � 1 ñîâïàäàþò, íî � 0 ÿâëÿåòñÿ �-ðåäåêñîì, à � 1 — �-ðåäåêñîì.  ÷àñò-
íîñòè, åñëè âõîæäåíèÿ � 0 è � 1 ÿâëÿþòñÿ ëèáî îäíîâðåìåííî �-ðåäåêñàìè, ëèáî
îäíîâðåìåííî �-ðåäåêñàìè, òî � �0 1� òîãäà è òîëüêî òîãäà, êîãäà ïåðâûé ñèì-
âîë èç � 0 ðàñïîëîæåí â t ñòðîãî ëåâåå, ÷åì ïåðâûé ñèìâîë èç � 1.
Îïðåäåëåíèå 11. Ñòðàòåãèåé ��-ëåâîé ðåäóêöèè íàçûâàåòñÿ ñòðàòåãèÿ f left
��
,
êîòîðàÿ ñâîðà÷èâàåò ñàìîå ëåâîå âõîæäåíèå ��-ðåäåêñà (åñëè ðàññìàòðèâàåìûé
�-òåðì íå íàõîäèòñÿ â ��-íîðìàëüíîé ôîðìå); àíàëîãè÷íî îïðåäåëÿåòñÿ ñòðàòå-
ãèÿ f left
�
�-ëåâîé ðåäóêöèè.
Óñëîâèìñÿ âìåñòî f t tleft
��
( ) �
ïèñàòü t t
left��
� �� ��
, à âìåñòî f t tleft
�
( ) �
—
ïèñàòü t t
left�
� ���
. Î÷åâèäíî, ñòðàòåãèè f left
��
è f left
�
ÿâëÿþòñÿ ��-îäíîøàãîâû-
ìè, ò.å. åñëè �-òåðì t íå ÿâëÿåòñÿ ��-íîðìàëüíîé ôîðìîé, òî èç t t
left��
� �� ��
ñëå-
äóåò, ÷òî t t�
��
. Åñëè, íàïðèìåð, îäíîâðåìåííî èìåþò ìåñòî ðåäóêöèè
t t
left��
� �� ��
è t t�
�
, òî áóäåì ïèñàòü t t
left�� �
� �� ��
.
Òåîðåìà íîðìàëèçàöèè äëÿ ��-ðåäóêöèè. Ñòðàòåãèÿ ��-ëåâîé ðåäóêöèè
ÿâëÿåòñÿ íîðìàëèçóþùåé.
Äîêàçàòåëüñòâî ïðîâåäåì îò ïðîòèâíîãî. Ïðåäïîëîæèì, ÷òî ñóùåñòâóåò òà-
êîé �-òåðì t, ÷òî t � ��-NF, íî f left
��
-ðåäóêöèîííàÿ öåïî÷êà
t t t t
left left left
� � �� �� � �� �� � �� ��
0 1 2�� �� ��
� (4)
íå ñîäåðæèò íè îäíîãî ÷ëåíà ti , ÿâëÿþùåãîñÿ ��-íîðìàëüíîé ôîðìîé. Ïîñ-
êîëüêó ñòðàòåãèÿ ��-ëåâîé ðåäóêöèè îäíîøàãîâàÿ, òî â ýòîé ðåäóêöèîííîé öå-
ïî÷êå êàæäûé �-òåðì ti
1 ïîëó÷àåòñÿ èç ïðåäûäóùåãî ñâîðà÷èâàíèåì ëèáî
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 61
�-ðåäåêñà, ëèáî �-ðåäåêñà. Òàê êàê ïîíÿòèå �-ðåäóêöèè ñèëüíî íîðìàëèçóåìî,
ðàññìàòðèâàåìàÿ ðåäóêöèîííàÿ öåïî÷êà ñîäåðæèò áåñêîíå÷íîå ÷èñëî ñâîðà÷è-
âàåìûõ âõîæäåíèé �-ðåäåêñîâ; â ñîîòâåòñòâèè ñ î÷åðåäíîñòüþ èõ ñâîðà÷èâà-
íèÿ îáîçíà÷èì èõ � � �0 1 2, , ,� Çàïèøåì öåïî÷êó (4) â âèäå
t t t t t ti
left
i i
left
i� � �� � ��
0 1 10
0
0 1
1
1
� ��
�� � �
�� �
� �
��
� ��
�� � �t ti
lef t
i2
2
2 1
�
� ��
� (5)
Ñîãëàñíî òåîðåìå î ��-íîðìàëüíîé ôîðìå �-òåðì t èìååò êàêóþ-òî �-íîðìàëü-
íóþ ôîðìó. Ïîñêîëüêó ñòðàòåãèÿ f left
�
�-ëåâîé ðåäóêöèè ÿâëÿåòñÿ íîðìàëèçóþùåé
(äîêàçàòåëüñòâî òåîðåìû íîðìàëèçàöèè äëÿ �-ðåäóêöèè ñì. â [1, c. 328–329]), áóäåò
ïîëó÷åíî ïðîòèâîðå÷èå ñ ëåììîé 3, åñëè äëÿ íåêîòîðîãî íàòóðàëüíîãî ÷èñëà n òà-
êîãî, ÷òî n m f sleft� ( , )
�
, óäàñòñÿ ïåðåñòðîèòü êàêîé-òî íà÷àëüíûé ñåãìåíò öåïî÷-
êè (5) â öåïî÷êó âèäà
t t t ti
left
i
lef t
i
le
�
� ��
� ��
� ��
0
0
1
1
2
2� � �' ' '
�
�
�
�
� ft
� �
� �
� �n
n
n
nleft
i
left
it t
� ���
� ���
2
2
1
1
' '
�
�
�
� ��� (6)
(çäåñü ïåðâûå n âõîæäåíèé ðåäåêñîâ
� � �0 1 1, , ,� n ÿâëÿþòñÿ ñàìûìè ëåâû-
ìè �-ðåäåêñàìè).
Âûáåðåì ëþáîå òàêîå íàòóðàëüíîå ÷èñëî n , ÷òî n m f sleft� ( , )
�
, è ðàññìîò-
ðèì íà÷àëüíûé ñåãìåíò öåïî÷êè (5), îêàí÷èâàþùèéñÿ ñâîðà÷èâàíèåì âõîæäåíèÿ
�-ðåäåêñà � n 1:
t t t t t ti
left
i i
left
i� � �� � ��
0 1 10
0
0 1
1
1
� ��
��
� �
��
�
� �
�� �
���
��
�t ti
left
in
in
n
� ���
1
1
1 1
�
. (7)
Äëÿ òîãî ÷òîáû ïðåîáðàçîâàòü (7) ê âèäó (6), âîñïîëüçóåìñÿ ïðèâîäèìîé íèæå
ëåììîé 4; ïðè ýòîì áåç óìàëåíèÿ îáùíîñòè ìîæíî ñ÷èòàòü, ÷òî â öåïî÷êå (7) ñâîðà-
÷èâàåòñÿ õîòÿ áû îäèí �-ðåäåêñ (èíà÷å ïîñòàâëåííàÿ öåëü óæå äîñòèãíóòà).
Ââåäåì ñëåäóþùèå âñïîìîãàòåëüíûå îáîçíà÷åíèÿ. Çàôèêñèðóåì êàêóþ-òî
îäíîøàãîâóþ ��-ðåäóêöèîííóþ öåïî÷êó p q�
�
. Åñëè w ÿâëÿåòñÿ âõîæäåíèåì
��-ðåäåêñà â p è èìååò åäèíñòâåííûé îñòàòîê ïðè ñâîðà÷èâàíèè �, òî ýòîò îñòà-
òîê îáîçíà÷èì w
�
. Àíàëîãè÷íî, åñëè w ÿâëÿåòñÿ âõîæäåíèåì ��-ðåäåêñà â q è ïðè
ýòîì ñóùåñòâóåò òàêîå åäèíñòâåííîå âõîæäåíèå ��-ðåäåêñà â p , êîòîðîå ïåðåõî-
äèò â w ïðè ñâîðà÷èâàíèè �, òî ýòî âõîæäåíèå îáîçíà÷èì w
�
; èíûìè ñëîâàìè,
w
�
— ýòî «êîîñòàòîê».
Ëåììà 4. Ïóñòü çàäàíà äâóõøàãîâàÿ ðåäóêöèîííàÿ öåïî÷êà âèäà
u
left
� � ��
� �� �
�
�
�� �1 2
1
, ïðè÷åì � �� �
�
�
1 . Òîãäà èìååò ìåñòî ñëåäóþùàÿ äèàãðàììà:
62 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4
�
�1
�1
� �
��
�-left
�-left
�
�
�
� �
1
� ��
�
�
�
u
ãäå âñåãäà �
�
1
�
ÿâëÿåòñÿ âõîæäåíèåì �-ðåäåêñà, à �
�
� — âõîæäåíèåì �-ðåäåê-
ñà. Ïðè ýòîì, åñëè òåðì �1 èìååò ñàìîå ëåâîå âõîæäåíèå �
�
1 �-ðåäåêñà, òî
� �
� �
�� �
1 .
Äîêàçàòåëüñòâî (ëåììû 4). Çàìåòèì, ÷òî ýòà ëåììà ÿâëÿåòñÿ ñïåöèàëüíûì
óòî÷íåíèåì òåîðåìû îá îòêëàäûâàíèè �-ðåäóêöèè. À èìåííî èç óñëîâèÿ
� �� �
�
�
1 ñëåäóåò, ÷òî ëèáî � �� �
�
1
�
� � , ëèáî � �� �
�
�
1 . Ýòè ñèòóàöèè ÿâëÿþòñÿ
ñîîòâåòñòâåííî ñëó÷àåì 1 è ïîäñëó÷àåì 3.1 èç äîêàçàòåëüñòâà òåîðåìû îá îòêëà-
äûâàíèè �-ðåäóêöèè. Âòîðîå óòâåðæäåíèå î÷åâèäíî.
Ëåììà äîêàçàíà.
Îïðåäåëåíèå 12. Ïóñòü çàäàíà êàêàÿ-òî êîíå÷íàÿ ��-ðåäóêöèîííàÿ öåïî÷êà
.
Îíà äîïóñêàåò åäèíñòâåííîå ïðåäñòàâëåíèå â âèäå
��
, ãäå
� — �-ðåäóê-
öèîííàÿ öåïî÷êà ìàêñèìàëüíîé äëèíû; öåïî÷êè
è
� íàçîâåì ñîîòâåòñòâåííî
òåëîì è õâîñòîì öåïî÷êè
.
Çàìåòèì, ÷òî â âûðîæäåííûõ ñëó÷àÿõ êàê òåëî, òàê è õâîñò öåïî÷êè
ìîãóò
îêàçàòüñÿ ïóñòûìè.
Íàêîíåö, ìîæåì ïðåîáðàçîâàòü öåïî÷êó (7) ê âèäó (6) è òåì ñàìûì çàêîí÷èòü
äîêàçàòåëüñòâî òåîðåìû íîðìàëèçàöèè äëÿ ��-ðåäóêöèè. Öåïî÷êó (7) îáîçíà÷èì
0 .
Çàìåòèì, ÷òî
0 ñîâïàäàåò ñî ñâîèì òåëîì è åå õâîñò ïóñò. Ïóñòü � �
0 — ïîñëåäíåå
âõîæäåíèå �-ðåäåêñà â
0 (áåç óìàëåíèÿ îáùíîñòè ìîæíî ñ÷èòàòü, ÷òî â öåïî÷êå (7)
ñâîðà÷èâàåòñÿ õîòÿ áû îäèí �-ðåäåêñ, òàê êàê èíà÷å óêàçàííàÿ öåëü óæå äîñòèãíóòà).
Èòåðàòèâíî ïðèìåíÿÿ ëåììó 4 ê � �
0 , ÷åðåç êàêîå-òî êîíå÷íîå ÷èñëî øàãîâ îòëîæèì
� �
0 â õâîñò ðåäóêöèîííîé öåïî÷êè. Ïîëó÷èì ��-ðåäóêöèîííóþ öåïî÷êó
1, â òåëå
êîòîðîé êîëè÷åñòâî ñâîðà÷èâàåìûõ �-ðåäåêñîâ íà åäèíèöó ìåíüøå, à êîëè÷åñòâî
ñâîðà÷èâàåìûõ �-ðåäåêñîâ — íà åäèíèöó áîëüøå, ÷åì â òåëå
0 . Îáîçíà÷èì � �
1 ïî-
ñëåäíåå âõîæäåíèå �-ðåäåêñà â òåëî öåïî÷êè
1. Ïîâòîðèâ óêàçàííûé ïðîöåññ îò-
êëàäûâàíèÿ � �
1 â õâîñò
1, îïÿòü ïîëó÷èì ��-ðåäóêöèîííóþ öåïî÷êó
2 , â òåëå êî-
òîðîé êîëè÷åñòâî ñâîðà÷èâàåìûõ �-ðåäåêñîâ íà åäèíèöó ìåíüøå, à êîëè÷åñòâî ñâî-
ðà÷èâàåìûõ �-ðåäåêñîâ íà åäèíèöó áîëüøå, ÷åì â òåëå
1. Àíàëîãè÷íî ïîñòðîèì
öåïî÷êè
3 ,
4 è ò.ä. Ñëåäîâàòåëüíî, äëÿ íåêîòîðîãî íàòóðàëüíîãî ÷èñëà k òåëî öå-
ïî÷êè
k ñîäåðæèò ðîâíî n ñâîðà÷èâàåìûõ �-ðåäåêñîâ è íå ñîäåðæèò ñâîðà÷èâàå-
ìûõ �-ðåäåêñîâ. Ýòî îçíà÷àåò, ÷òî
k — èñêîìàÿ öåïî÷êà âèäà (6).
Òåîðåìà íîðìàëèçàöèè äëÿ ��-ðåäóêöèè äîêàçàíà.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Á à ð å í ä ð å ã ò Õ. �-èñ÷èñëåíèå. Åãî ñèíòàêñèñ è ñåìàíòèêà. — Ì.: Ìèð, 1985. — 606 ñ.
2. C u r r y H . B . , F e y e s R . , C r a i g W . Combinatory logic. — Amsterdam: North-Holland., 1958. — 1.
3. C u r r y H . B . , H i n d l e y J . R . , S e l d i n J . P . Combinatory logic. — Amsterdam: North-Holland,
1972. — 2.
4. B a r e n d r e g t H . P . , B e r g s t r a J . , K l o p J . W . , V o k e n H . Some notes on lambda reduction //
Degrees, reductions, and representability in the lambda calculus. — Utrecht: Univ. of Utrecht, Dep. of
Math., 1976. Preprint N 22. — P. 13–53.
5. K l o p J . W . Combinatory reduction systems // Ph.D. Thesis. — Utrecht: Utrecht univ., 1980. — 323 p.
Ïîñòóïèëà 17.06.2013
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2014, òîì 50, ¹ 4 63
|