ББК 22.12

Б 24
УДК 510.2, 510.6

Барендрегт X.

Б 24   Ламбда-исчисление. Его синтаксис и семантика: Пер.
с англ.—М.: Мир, 1985.—606 с.

Монография посвящена классическим и новым результатам в активно раз-
вивающемся направлении математической логики,- так называемом ламбда-ис-
числении Оно находит применение в теории доказательств, семантике языков
программирования, алгебре, топологии, теории категорий. Изложение отлича-
ется полнотой и доступностью. Автор книги — известный голландский ма-

тематт1к^ ц^^ятиков разных специальностей, преподавателей, аспирантов и

студентов университетов.

1702020000—434

10—84, ч. 1

041(01)—85

ББК 22.12
517

Редакция литературы по математическим наукам

© North-Holland    Publishing.:

Company, 1981

© Перевод на русский язык,
«Мир», 1985

Предисловие к русскому изданию

Книга профессора Утрехтского университета X. Барендрег-
та — первое на русском языке подробное и доступное изложение
ламбда-исчисления. Возникнув в основаниях математики, эта си-
стема была построена как теория вычислений с естественной
бестиповой операционной семантикой. Она стала объектом осо-
бенно пристального внимания в информатике после того, как
выяснилось, что ламбда-исчисление представляет собой удобную
модель, выявляющую многие важные аспекты построения и ра-
боты программ, написанных на алгоритмических языках. В пре-
дисловии А. П. Ершова к переводу книги П. Хендерсона «Функ-
циональное программирование» (М.: Мир, 1983) прямо гово-
рится, что «ламбда-исчисление... сейчас можно считать не чем
иным, как теоретической моделью современного функциональ-
ного программирования».

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

Нашла приложения и важная модификация ламбда-исчисле-
ния, называемая чистой комбинаторной логикой, в которой пере-
менные не используются и применяются комбинации всего двух
символов К, S, подчиненных всего двум определяющим равен-
ствам: (КА)В==А, ((SA)B}C==(AC){BC).

Такая система возникла в начале 20-х годов и восходит к
советскому математику М. И. Шейнфинкелю '), дальнейшее раз-
витие она получила в трудах X. Карри, А. Чёрча и др.

') См. также обзор С. А. Яновской «Основания математики и математиче-
ская логика» (сб. «Математика в СССР за тридцать лет», М.-Л.: !948,
с. 11—45).

Литература

Акцель (Aczel P.)

[1980] Frege structures and the notions of proposition, truth and set.

В кн.: Барвайз и др. [1980], с. 31—60.
Арбиб, Мейнс (Arbib M. A., Manes E. G.)

[1975] Arrows, Structures and Functors. Academic Press, New York.
Аусьелло, Бём (Ausiello G., Bohm C. (eds.))

[1978] Automata, Languages and Programming. Fifth Colloquim, Udine,
Italy, July 1978, Lecture Notes in Computer Science 62, Spring-
er-Verlag, Berlin.
Ашкрофт, Хеннесси (Aschcroft E. A., Hennessy M. C.B.)

[1980] A mathematical semantics for a non deterministic typed lambda

calculus. Theor. Comput. Sci. 11, pp. 227—245.
Бандер (Bunder M. W.)

[1974]   Some inconsistencies in illative combinatory logic. Z. Math. Lo-
gic Grundlang. Math. 20, pp. 71—73.

[1980] The naturalness of illative combinatory logic as a basis for ma-
thematics. В кн.: Хиндли, Селдин [1980J, с. 55—64.

[1981] Predicate calculus and naive set theory based on pure combina-
tory logic. Arch math. Logik Grundlagenforsch. 21, pp. 169—177.
Барвайз (ред.) (Barwise J. (ed.)).

[1977] Handbook of Mathematical Logic, Studies in Logic 90, North
Holland Amsterdam. [Имеется перевод: Справочная книга по
математической логике в 4-х т.—M.: Наука, 1982—1983.]

[1977а] An introduction to first order logic. В кн.: Барвайз [1977],

с. 5—46.

Барвайз и др. (ред.) (Barwise J. et al.-Barwise J., Keisler H. J., Kunen K.
(eds.))

[1980] The Kleene Symposium. Studies in Logic 101. North-Holland,

Amsterdam.
Барендрегт (Barendregt H. P.)

[1971] Some Extensional Term Models for Combinatory Logics and
^.-calculi. Dissertation. University of Utrecht.

[1973] Combinatory logic- and the axiom of choice. Indag. Math. 35,
pp. 203—221.

[1973a] A characterization of terms of the ^.-/-calculus having a normal
form. J. Symbolic Logic, 38, 441—445.

[1974] Pairing without conventional restraints. Z. Math. Logik Grund-
lag. Math, 20, pp. 289—306.

[1974a] Combinatory logic and the co-rule. Fundamenta Math. 82,
pp. 199—215.

[1975] Normed uniformly reflexive structures. В кн.: Бём [1975],
с. 272—286.

[1976] A global representation of the recursive functions in the lambda
calculus. Theor. Comput. Sci. 3, pp 225—242.

[1977] The type free lambda calculus. В кн.: Барвайз [1977], с. 1092—
1132.

Литература                           573

Барендрегт и др. (Barendif^t H, P. et al. = Barendregt H. P., Bergstra J.,

Klop J. \V., Volken H.)

[1976] Some notes on lambda reduction. In: Degrees, reductions and
representability in the lambda calculus. Preprint no. 22, Univer-
sity of Utrecht, Department of Mathematics, pp. 13—53.
[1976a] Representabilitv in lambda algebras. Indag. Math. 38, pp. 377—

387.
[1978] Degrees of sensible lambda theories. J. Symbolic Logic 43,

pp. 45—55.
Барендрегт, Койманс (Barendregt H. P., Koymans К.)

[1980] Comparing some classes of lambda calculus models. В кн.: Хинд-
ли, Селдин [1980], с. 287—302.
Варендрегт, Коппо, Дедзани-Чанкальинп (Barendregt H. P., Coppo M., Dezani-

Ciancaglini M.)
[1983] A filter lambda model and the completeness of type assignment.

J. Symbolic Logic, to appear.
Барендрегт, Лонго (Barengdrcgt H. P., Longo G.)

[1980] Equality of ^-terms in the model Т"- В кн.: Хиндли, Селдин

[1982], с. 287—302.
[1982] Recursion theoretic operators and morphisms of numbered sets.

Fund. Math. CXIX, to appear.
Батен, Бурбом (Baeten J., Boerboom B.)

[1979] Q can be anything it should'nt be. Indag. Math. 41, pp. Ill—

120.
Бел M. (Bel M.)

[1977] An intuitionistic combinatory theory not cosed under the rule

of choice. Tndag. Math. 39, pp. 69—72.
Беманн (Behmann H.)

[1922] Beitrage zur Algebra der Logik, insbesondere zum Entschei-

dungsproblem. Math. Annalen 86, pp. 163—229.
Бём (Bohm С.)

[1968] Alcune proprieta delle forme P-T| normali nel ^.-/(-calcolo. Publl-
cazioni dell'Istituto per le Applicazioni del Calcolo. n. 696,
Roma (19).
Бём (ред.) (Bohm S. (ed.))

[1975] ^-calculus and Computer Science Theory. Proceedings of the
Symposium held in Rome. March 25—27, 1975, Lecture Notes in
Computer Science 37, Springer-Verlag, Berlin.
Бём, Дедзани-Чанкальини (Bohm С., Dezani-Ciancaglini M.)

[1972] Can syntax be ignored during translation? В кн.: Нива [1972],

с. 197—207.
[1974] Combinatorial problems combinator equations and normal forms.

В кн.: Локс [1974], с. 185—199.
[1975] X-Terms as total or partial functions on normal forms. В кн.:

Бём [1975], с. 96—121.
ван Бентхем Ю. Ф. А. К. (van Benthem J. F. А. К.)

[1978] Four paradoxes. J. Philos. Logic 7, pp. 49—72.
ван Бентхем Юттинг Л. С. (van Benthem Jutting t. S.)

[1979] Checking Landau's «Grundlagen» in the Automath System. Ma-
thematical Centre Tracts, Mathematical Centre, Amsterdam.
Бергстра, Клоп ^Bergstra J., Klop J. W.)

[l(/79] Church—Rosser strategies in the lambda calculus. Theor. Com-
put. Sci. 9, pp. 2"—38.
[1980] Invertible terms in the lambda calculus. Theor. Comput. Sci. 11,

pp. 19—37.

[1982] Strong normalization and perpetual reductions in the lambd.'i
calculus. J. Information Processing and Cybernetics, 18, no. 7—f
pp. 403—417.

576 Литература

[1982a] Conditional rewrite rulas: confluency and termination. Preprint,
Mathematical Center, Kruislaan 413, 1098 SJ Amsterdam, The
Netherlands.
Бёрдж (Burge W.)

[1978] Recursive Programming Techniques. Addison-Wesley, Reading,

MA.
Берклинг, Фер (Berkling К. J., Fehr E.)

[1982] A modification of the lambda calculus as a base for functional
programming languages. В кн.: Нильсен, Шмидт [1982], с. 35—
47.
Берри (Berry G.)

[1978] Sequentialite de revaluation formelle des ^-expressions. In: Proc.
3-e Colloque International sur la Programmation, Paris, mars
1978, Dunod, Paris.
Бизон (Beeson M.)

[198—) Foundations of constructive mathematics. Mathematical studies,
Springer, Berlin, to appear.

Боллобаш (Bollobas B.)

[1979] Graph Theory, Springer-Verlag, Berlin.
Боффа ван Дален, Мак-Алун (ред.) (Boffa M., van Dalen D., McAloon K.

(eds.))

[1980] Logic Colloquium'78, Studies in Logic 97. North-Holland, Am-
sterdam.

де Брёйн (de Bruijn N. G.)

[1970] The mathematical language Automath, its usage and some of its
extensions, in: Symposium on Automatic Demonstration, IRIA,
Versalles Dec. 1968, Lecture Notes in Mathematics 125, Springer-
Verlag, Berlin, pp. 25—61.

[1972] Lambda calculus notation with nameless dummies, a tool for
automatic formula manipulation. Indag. Math. 34, pp. 381—392.

[1980] A survey of the project Alitomath. В кн.: Хиндли, Селдин [1980],

с. 579—607.
Вагнер (Wagner E.)

[1969] Uniform reflexive structures: on the nature of Godelizations and
relative computability. Trans. Amer. Math. Soc. 144, pp. 1—41.

Вегнер (Wegner P.)

[1972]  The Vienna Definition Language, ACM Computing Surveys 4.
Виссер (Visser A.)

[1980] Numerations, ^.-calculus and arithmetic. В кн.: Хиндли, Селдин

[1980], с. 259-284.
Ганди (Gandy R. О.)

[1980]  An early proof of normalisation by A. M. Turing. В кн.: Хиндли,

Селдин [1980], с. 453—456.
Ганди, Иетс (ред.) (Gandy R. О., Yates С. M. E, (eds.))

[1971] Logic Colloquium'69. Studies in Logic 61, North-Holland, Am-
sterdam.
Гейтинг (ред.) (Heyting A. (ed.))

[1959] Constructivity in Mathematics. North-Holland, Amsterdam.
Генцен (Gentzen G.)

[1969] The Collected Papers of Gerhard Gentzen, Edited by M. E. Sza-
bo, North-Holland, Amsterdam, [Переводы большинства работ
имеются в кн.: Идельсон, Минц [1967].]
Гёдель (Gode! К.)

[1958] Ober eine bisher noch nicht benutzte Erweiterung des finiten
Standpunktes. Dialectica 12, pp. 280—287. [Имеется перевод:

Гёдель К. Об одном еще не использованном расширении фи-
нитной точки зрения.—В кн.: Идельсон, Минц [1967], с. 299—
305.]

Литература                          577

Гийом (ред.) (Guillaunip M. (ed))

[1977] Colloque International de Logique, Clermont-Ferrand 18—25

Juillet 1975, CNRS. Paris.

Гирц и др. (Gierz G. et al. = Gierz G., Lawson J. D., Hofmann К Н Mis-
love M„ Keimel K., Scott D. S.)

[198.0] A Compendium of Continuous Lattices. Springer-Verlag, Berlin.
Говард (Hoyard W.)

[1968] Functional interpretation of bar induction by bar recursion

Сотр. Math. 20, pp. 107—124.
[1980] The formulae-as-types notion of construction. В кн: Хиндли,

Селдин [1980], с. 479—490.
Гордой (Gordon M. J. С.)

[1973] Evaluation and Denotation of Pure LISP: a Worked Example

in Semantics, Dissertation, University of Edinburg.
[1979]  The Denotational Description of Programming Languages

Springer-Verlag, Berlin.

Гордон H др. (Gordon M. J. C. et al. = Gordon M. J. C., Milner R., Wads-
worth C.)
[1979] Edinburgh LCF. A Mechanical Logic of Computation. Lecture

Notes in Computer Science 78. Springer-Verlag, Berlin.
ван Дален (van Daalen D. T.)

[1980] The Language Theory of Automath, Dissertaion, Technological

University Eindhoven.
ван Дален и др. (van Dalen D. et al. = van Dalen D., Doets H C

de Swart H. C. M.)

[1978] Sets. Naive, Axiomatic and Applied. Pergamon Press, New York.
Дедзани-Чанкальини (Dezani-Ciancaglini M.)

[1976] Characterization of normal forms possessing inverse in the

^.-p-T)-calculus. Theor. Comput. Sci. 2, pp. 323—337.
Дедзани-Чанкальини, Монтанари (ред.) (Dezani-Ciancaglini M., Montanari U

(eds.))
[1982] International symposium on programming. Lecture Notes in

Computer Science 137, Springer-Verlag, Berlin.
Деккер (ред.) (Dekker J. C. E. (eds.))

[1962] Recursive function theory. Proceedings of Symposia in Pure Ma-
thematics, Vol. 5, Amer. Math. Soc. Providence, RI.
Дершовиц (Dershowitz N.)

[1982] Orderings for term rewriting systems. Theor. Comput. Sci. 17,

pp. 279—301.
Джаннини, Лонго (Giannini P., Longo G.)

[1983] Effectively given domains and lambda calculus semantics. Pre-
print, Dipt. Informatica, Corso Italia 40, 561100, Pisa, Italy.
Диллер, Мюллер (ред.) (Diller J., Muller G. H. (eds.))

[1975] ISILC. Proof Theory Symposium. Lecture Notes in Mathematics

500, Springer-Verlag, Berlin.
Диллер, Фогель (Diller J., Vogel H.)

[1975] Intensionale Funktionalinterpretation der Analysis. В кн.: Дил-
лер, Мюллер [1975], с. 56—72.
Донахью (Donahue J.)

[1979] On the semantics of «data type». SIAM J. Сотр. 8, 544—560.
Драгалин А. Г.

[1968] Вычислимость примитивно рекурсивных термов конечного типа
и примитивно рекурсивная реализация. — Записки научн. сем.
Лен. отд. Матем. ин-та им. В. А. Стеклова АН' СССР, т. 8,
с. 32—45.
Ершов Ю. Л.

[1973/75/77] Theorie der Numerierungen. Z. Math. Logik Grundlag Math.
19 (1973), S. 289—388; 21 (1975); S. 473—584; 23 (1977),
S. 289-371                                     .     \    г

19 X. Варендрегт

578 Литература

[1977] Теория нумераций.— М.: Наука.
Жирар (Girard J.-Y.)

[1971] Une extension de 1'interpretation de Godel a 1'analyse et son
application a i'elimination des cuupures dans 1'analyse et la
theorie des types. В кн.: Фенстад [1971], с. 63—92.
Идельсон А. В., Минц Г. Е (ред.)

[1967] Математическая теория логического вывода.—М.: Наука.
Кальмар (Kalmar L.)

[1937] Zuruckfiihrung des Entscheidungsproblem auf den Fall von For-
mein mit einer einzigen binaren Funktionsvariablen. Comp.Matli
4, pp. 137—144.
Кангер (ред.) (Kanger S. (ed.))

[1975] Proceedings of the Third Scandinavian Logic Symposium. Stu-
dies in Logic 82, North-Holland, Amsterdam.
Карри (Curry H. B.)

[1930] Grundlagen der Kombinatorischen Logik. Amer. J. Math. 52,

pp. 509-536, 789—834.
Карри и др. (Curry H. В. et а1. == Curry H. В., Feys R., Craig W.)

[1958] Combinatory Logic, Vol. I. North-Holland, Amsterdam.
Карри и др. (Curry H. В. et al. = Curry H. В., Hindley J. R., Seldin J. P.)
[1972] Combinatory Logic, Vol. II. Studies in Logic 65, North-Holland,

Amsterdam.
Келли (Kelley J. L.)

[1955] General Topology. D. van Nostrand. Princeton. [Имеется пере-
вод: Келли Дж. Общая топология.—М.: Наука, 1981.]
Клини (Kleene S. С.)

[1936] ^-definability and recursiveness. Duke Math. J. 2, pp. 340—353.
[1952]  Introduction to Metamathematics. P. Noordhof N. V., Groningen
[Имеется перевод: Клини С. К. Введение в метаматематику. —
М.: ИЛ., 1957]
[1961/1962] Lambda definable functionals of finite tipes. Fundamenta

Math. 50, pp. 281—303.
Клини, Poccep (Kleene S. С., Rosser J. B.)

[1935] The inconsistency of certain formal logics. Annals of Math.

(2) 36, pp. 630—636.
Клоп (Klop J. W.)

[1975] On solvability by ^-/-terms. В кн.: Бём fl975], с. 342—345.
[1980] Combinatory reduction systems. Mathematical Centre Tracts 127,

Amsterdam.
[1980a] Reduction cycles in combinatory logic. В кн.: Хиндли, Селдин

[1980], с. 193—214.
[1982] Extending partial combinatory algebras. Bull. European Ass.

Theor. Comput. Sci. 16, pp. 30—34.
Кнастер (Knaster B.)

[1928] Un theoreme sur les fonctions d'ensembles. Annales. Soc. Pol.

Math. 6, pp. 133—134.
Кнут (Knuth D. E.)

[1970] Examples of formal semantics, in: Engeler E. (ed.). Symposium
on Semantics and Algorithmic Languages, Lectures Notes in
Mathematics 188, Springer-Verlag, Berlin.
Койманс (Koymans K.)

[1979]  Lambda Calculus Models, Master thesis, University of Utrecht,

Mathematisch Inst.

[1983] Models of the lambda calculus. Inform. Control, to appear.
Коппо (Сорро М.)

[198—] Completeness of type assignment in continuous lambda models.
Theor. Comput. Sci., to appear

Литература                            579

Коппо и др. (Сорро М., Dezani-Ciancaglini N.. Ronci della Rocca S.)

[1978] Semiseparability of finite sets of terms in Scott's Doe-models of

the ^.-calculus. В кн.: Аусиелло, Бём [1978], с. 142—164.

Коппо и др. (Сорро М. et al. = Сорро М., Dezani-Ciancaglini M., Venneri В.)
[1980] Principal type schemes and Л-calculus semantics, В кн.: Хиндли,

Селдин [1980], с. 535—560.
Коппо и др. (Сорро М. et al. = Сорро М., Dezani-Ciancaglini M., Honsell F.,

Longo G.)
[1983] Extended type structures and filter lambda models. В кн.: Лон-

го и др.-[1983].
Коэн и др. (ред.) (Cohen L. J. et al. = Cohen L. J., Los J., Pfeiffer H.. Po-

dewski K..-P. (eds.))

[1982] Logic, Methodology and Philosophy of Science VI. North-Hol-
land, Amsterdam.
Крайзель (Kreisel G.)

[1959] Interpretation of analysis by means of constructive functionals

of finite types. В кн.: Гейтинг [1959], с. 101—128.
[1971]  Some reasons for generalizing recursion theory. В кн.: Ганди,

Итс [1971], с. 139—198.
Кроссли (ред.) (Crossley J. N. (ed.))

[1975]  Algebra and Logic. Lecture Notes in Mathematics 450, Springer-
Verlag, Berlin.
Кроссли, Дамметт (ред.) (Crossley J. N., Dummett M. A. E. (eds.))

[1965] Formal Systems and Recursive Functions. Pros. 8th Logic Collo-
quium, Oxford, July 1963, North-Holland, Amsterdam.
Кузичев A. C. (Kuzichev A. S.)

[1980] Sequential systems of lambda conversion and of combinatory

logic. В кн.: Хнндли, Селдин [1980], с. 141—155.

[1983] Арифметически непротиворечивые л-теории бестиповой логи-
ки.—ДАН СССР, т. 268, № 2, с. 288—292.
Ламбек (Lambek J.)

[1980] From X-calculus to cartesian closed categories. В кн.: Хиндли,
Селдин [1980], с. 375—402.

Ламбек, Скотт (Lambek J., Scott P. J.)

[1982] Cartesian closed categories and lambda calculus, preprint. Dept.

of Mathematics, McGill University, Montreal, Canada,
Ландин (Landin P. J.)

[1965] A correspondence between ALGOL 60 and Church's lambda no-
tation. Comm. Assoc. Comput. Math. 8, pp. 89—101, 158—165.

[1966] A A-calculus approach, in: Advances in Programming and Non-
numerical Computation. Pergamon Press, New York, pp. 97—141.

[1966a] The next 700 programming languages. Comm. Assoc. Comput.

Mach. 9, pp. 157—164.
Леви (Levy J.-J.)

[1975] An algebraic interpretation of the Т.-р-Я-calculus and a labelled
^.-calculus. В кн.: Бём, [1975], с. 147—165.

[1978] Reductions correctes et optimales dans le lambda calcul, These
de doctoral d'etat. Universite Paris VII.

[1980] Optimal reductions in the lambda calculus. В кн.: Хиндли, Сел-
дин [1980], с. 159—192.
Лёрчер (Lercher B.)

[1963]   Strong Reduction and Recursion in Combinatory Logic. Disser-
tation, The Pennsylvania State University.

[1967] The decidability of Hindley's axioms for strong reduction. J.

Symbolic Logic'32, pp. 237—239.
Лёб (Lob M. H.)

[1955] A colution of a problem of Henkin. J. Symbolic Logic 20,
pp. 115—118.

19*

580 Литература

Ливер (Lawvcre F. \V. (ed.))

[1972] Toposes, Algebraic Geometry and Logic. Lecture Notes in Ma-
thematics 274, Springer-Verlag, Berlin.
Лоиго (Longo G.)

[1983] Set theoretical models of lambda calculus: theories, expansions

and isomorphisms. Ann. Pure Appl. Logic 24, pp. 153—188.
Лонго и др. (ред.) (Longo G. et al. = Longo G., Lolli G., Marcija A. (eds))

[1983] Logic Colloquium'82. North-Holland, Amsterdam.
Луке (ред.) (Loeckx J. (ed.))

[1974] Automata, Languages and Programming. 2nd Colloquim, Univer-
sity of Saarbnicken, 1974, Lecture Notes in Computer Science 14,
Springer-Verlag, Berlin.
Лукхардт (Luckhardt H.)

[1973] Extensional Godel Functional Interpretation. A Consistency
Proof of Classical Analysis. Lecture Notes in Mathematics 306
Springer-Verlag, Berlin.
Маккарти (McCarthy J.)

[1962] The LISP 1.5 Programmer's Manual. MIT Press, Cambridge, MA.
Маклейн (MacLane S.)

[1972] Categories for the Working Mathematician. Springer-Verlag, Ber-
lin.
Манн (Mann C. R.)

[1975] The connection between equivalence of proofs and cartesian clos-
ed categories. Proc. London Math. Soc. (3) 31, pp. 289—310
Мартин-Лёф (Martin-Lot P.)

[1982] Constructive mathematics and computer programming В кн •

Коэн и др. [1982], с. 153—178.
Мейер (Меуег А.)

[1982] What is a model of the lambda calculus? Information Control

52, pp. 87—122.
Мередит, Прайор (Meredith С. A., Prior A. N.)

[1963] Notes on the axiomatics of propositional calculus. Notre Dame J

Formal Logic 4, pp. 172—187.
Милн, Стрейчи (Milne R. ., Strachey С.)

[1976] A Theory of Programming Language Semantics, 2 vols. Chap-
man and Hall, London; Wiley, New York.
Минц Г. Е.

[1979] Теория категорий и теория доказательств.—В кн.: Актуальные
проблемы логики и методологии науки. — Киев: Наукова дум-
ка, с. 252—278.
Мнчке (Mitschke G.)

[1976] ^-Kalkul, S-Konversion und axiomatische Rekursionstheorie Pre-
print Nr. 274, Technische Hochschule, Darmstadt. Fachbereit Ma-
thematik, 77 pp.
[1979] The standartization theorem for the ^.-calculus Z Math Loeik

Grundlag. Math. 25, pp. 29—31.
Моррис- (Morris J.-R)

[1968] Lambda Calculus Models of Programming Languages. Disserta-
tion, M. I. T.
Мурский В. Л.

[1967] Изоморфная вложимость полугрупп со счетным множеством
определяющих соотношений в конечно представнмые полугруп
пы. Матем. заметки, т. I, с. 217—224.
Накадзима (Nakajima R.)

[1975] Infinite normal forms for the A-culculus В кн • Бём Г19751

с. 62—82.                                       '       i    J-
Нива (ред.) (Nivat M. (ed.))

[1972] Automata, Languages and Programming. North-Holland Amster-
dam.

Литература                          581

Нильсен, Шмидт (ред.) (Nielsen N., Schmidt E. M. (eds.))

[1982] Automata, Languages and Programming. Lecture Notes in Comp-
uter Science 140, Springer-Verlag, Berlin.
Ныоман (Newman M. N. A.)

[1942] On theories with a combinatorial definition of «Equivalence».

Ann. of Math. (2) 43, pp. 223—243.
0'Доннелл (O'Donnell M. J.)

[1977] Computing in Systems Described by Equations. Lecture Notes in

Computer Science 58, Springer-Verlag, Berlin.
Оллонгрен (Ollongren A.)

[1975] A Definition of Programming Languages by Interpreting Auto-
mata. Academic Press, New York and London.
Парих Р. (ред.) (Parikh R. (ed.))

[1975]  Logic Colloquium, Sysposium on Logic Held at Boston, 1972—
1973. Lecture Notes in Mathematics 453, Springer-Verlag, Berlin.

Парк (Park D.)

[1976] The У-combinator in Scott's Lambda Calculus Models (revised
version). Theory of Computation Report No. 13; University of
Warwick, Dept. of Compul. Sci.

Петер (Peter R.)

[1967] Recursive Functions. Academic press, New York and London.
[Имеется перевод предыдущего издания: Петер Р. Рекурсивные
функции.—M.: ИЛ, 1954.]

Плоткин (Plotkin G. D.)

[1972]  A Set-theoretical Definition of Application. School of Artificial

Intelligence, Memo MIP-R-95, University of Edinburgh.
[1974] The ^-calculus is to-incomplete. J. Symbolic Logic 39, pp. 313—

317.
[1975] Call-by-name, call-by-value and the А.-calculus. Theor. Comput.

Sci. 1, pp. 125—159.

[1976] A powderdomain construction. SIAM J. Comput. 5, pp. 452—487.
[1977] LCF as a programming language. Theor. Comput. Sci. 5,

pp. 223—257.
[1978] T as a universal domain. J. Comput. Syst. Sci 17, pp. 209—

236.
Плоткин, Смит (Plotkin G. D., Smyth M. B.)

[1978] The category-theoretic solution of recursive domain equations.

DAI Research Report 60, University of Edinburgh.
ван дер Поль и др. (van der Poel W. L., et al. == van der Poel W. L.,

Schaap C. E., van der Mey G.)
[1980] New Arithmetical Operators in the Theory of Combinators. Indag.

Math. 42, pp.

Поттингер (Pottinger G.)

[1977] Normalization as a homomorphic image of cut elimination. Ann.
Math. Logic 12, pp. 323—357.

Проблемы (Problems)

[1975] Open problems. В кн.: Бём [1975], с. 367—370.
[1980] Open problems. Bull. European Ass. Comput. Sci. 13(5),

pp. 308—319.
Резус (Rezus A.)

[1982] A bibliography of lambda calculi, combinatory logic and related

topics. Mathematical Centre Tracts, Amsterdam.
[1982a] On a theorem of Tarski. Libertas Math. 2, pp. 63—97.
Рейнольдс (Reynolds J. C.)

[1970] GEDANKEN—A simple typeless language based on principle
of completeness and reference concept. Comm. Assoc. Comput.
Mach. 13(5), pp. 308-319.

"582

Литература

Роджерс (Rogers H.)

[1967] Theory of Recursive Functions and Effective Operations. McGraw
Hill, New York. [Имеется перевод: Роджерс X. Теория рекур-
сивных функций и эффективная вычислимость.—М.: Мир,
1972.]

[1973] The manipulation systems and the Church-Rosser theorem. J.
Assoc. Comput. Mach. 20, pp. 160—187.

Poccep (Rosser J. B.)

[1935] A mathematical logic without variables. Annals of Math. (2) 36,

pp. 127—150; Duke. Math. J. 1, pp. 328—355.
Роуз, Шепердсон (ред.) (Rose H. E., Sheperdson J. C. (eds.))

[1975] Logic Colloquium'73. Studies in Logic 80, North-Holland, Am-
sterdam.
Сабо (Szabo M. E.)

[1978] Algebra of Proofs. Studies in Logic 88, North-Holland, Amster-
dam.
Санчис (Sanchis L. E.)

[1967] Functionals defined by recursion. Notre Dame J. Formal Logic 8

pp. 161—174.

[1979] Reducibilties in two models for combinatory logic. J. Symbolic
Logic 44, pp. 221-^234.

Селдин (Seldin J. P.)

[1976/7] Recent advances in Curry's program. Rend. Sem. Mat. Univers.

Politecn. Torino 35, pp. 77—88.

[1979] Progress report on generalized functionality. Ann. Math. Lo-
gic 17, pp. 29—59.
Скарпеллини (Scarpellini В.)

[1971] A model for bar recursion of higher types. Сотр. Math. 23,

pp. 123—153.
CKOTT (Scott D. S.)

T963] A system of functional abstraction (unpublished).

T969] Models for the ^.-calculus. Manuscript (unpublished), 53 pp.

T972] Continuous lattices. В кн.: Ловер [1972], 97—136.

'1973] Models for various type free calculi. В кн.: Супис и др. Г19731

с. 157-187.
[1974] The language LAMBDA (abstract). J. Symbolic Logic 39

pp. 425—427.
[1975] Lambda calculus and recursion theory. В кн.: Кангер [19751,

с. 154-193,

[1975a] Combinators and classes. В кн.: Бём [1975], с. 1—26.
[1975b] Some philosophical issues concerning theories of combinators

В кн.: Бём [1975], с. 346—366.
[1976] Data types as latices. SIAM J. Comput. 5, pp. 522—587.
[1980] Lambda calculus: some models, some philosophy В кн : Барвайз

и др. [1980], с. 223—266.
[1980а] Relating theories of the A.-calculus. В кн.: Хинвди, Селдин

[1980], с. 403—450.
[1982] Domains for denotational semantics. В кн.: Нильсен, Шмидт

[1982], с. 577—613
Скотт, Стрейчи (Scott D. S., Strachey С.)

[1971] Toward a mathematical semantics for computer languages. Pro','.

Symp. on Computers and Automata, Polytechnic Institute of

Brooklyn, 21, pp. 19—46.

Спектор К. (Spector С.)

[1962]  Provably recursive functionals of analysis: a consistency proof
of analysis by an extension of principles formulated in current
Intuitionistic mathematics. В кн.: Деккер [1962], с. 1—27.

Литература                          583

Степлз (Staples J.)

[1975] Church— Rosser theorems for replacement svstems. В кн.: Крос-

сли, [1975J, с. 291—307.
Стетмен (Statman R.)

[1979] The typed ^,-calculus is not elementary recursive. Theor. Com-
put. Sci. 9, pp. 73—81.
[1980]  On the existence of closed terms in the typed lambda calclus I.

В кн.: Хипдли, Селдин [1980], с. 511—534.
[1981] On the existence of closed terms in the typed lambda calculus II:

transformations of unification problems. Theor. Comput. Sci. 15,
pp. 329—338.
[1982] Completeness, invariance and ^-definability. J. Symbolic logic 47,

no. 1, pp. 17—26.
Стой (Stoy J. E.)

[1977] Denotational Semantics. The Scott-Strachey approach to Pro-
gramming Languages. MIT Press, Cambridge.
Стронг (Strong H.)

[1968] Algebraically generalized recursive function theory. IBM J. Re-
search Develop. 12, pp. 465—475.
Супис и др. (ред) (Suppes P. et al. = Suppes P., Henkin L., Joja A., Moisil,

Gr. С. (eds.))

[1973] Logic, Methodolgy and Philosophy of Science IV. Studies in Lo-
gic 74, North-Holland, Amsterdam.
Тарский (Tarski A.)

[1955]  A lattice-theoretical fixed point theorem and its applications.

Pacific J. Math. 5, pp. 285—309.
Тейт (Tait W.)

[1965]  Infinitely long terms of transfinite type. В кн.: Кроссли, Дам-

метт [1965], с; 176—185.

[1967] Intensional interpretations of functionals of finite type I. J. Sym-
bolic Logic 32, pp. 198—212.
[1971] Normal form theorem tor barrecursive functions of finite type.

В кн.: Фенстад [1971], с. 353—367.
Терлув (Terlouw J.)

[1982] On difinition trees of ordinal recursive functionals: reduction of
orders by means of type level raisings. J. Symbolic Logic 47,
no. 2, pp. 295—403.
Тернер (Turner D. A.)

[1979] A new implementation technique for applicative languages. Soft-
ware—Practice and Experience 9, pp. 31—49.
Трулстра (ред.) (Troelstra A. S. (ed.))

[1973] Metamathematicai Investigations of Intuitionistic Arithmetic and
Analysis. Lecture Notes in Mathematics 344, Springer-Verlag,
Berlin.

Трулстра (Troelstra A. S.)

[1975] Nonextensional equality. Fundamenta Math. 82, pp. 307—322.
Трулстра, ван Дален (ред.) (Troelstra A. S., van Dalen D. (eds.))

[1982] The L. E. J. Brouwer centenary symposium. North-Holland, Am-
sterdam.
Тьюринг (Turing A. M.)

[1936] On computable numbers with an application to the Entschei-

dungsproblem. Proc. London.Math. Soc. 42, pp. 230—265.
[1937] Computability and ^.-definability. J. Symbolic Logic 2, pp. 153—

163.

[1937a] The y-iunctions in ^.-A'-conversion. J. Symbolic Logic 2, p. 164.
Уодсворт (Wadsworth С. Р.)

[1971] Semantics and Pragmatics of the Lambda-calculus. Dissertation,
Oxford University.

584 Литература

[1976] The relation between computational and dcnotational properties
for Scott's Doo-models of the lambda-calclus. SIAM J. Comput 5
pp. 488-521.

[1980] Some unusual ^.-calculus numeral systems. В кн.: Хиндлп, Сел-
дин [1980], с. 215—230.
Уэлч (Welch Р. Н.)

[1975] Continuous semantics and inside out reductions. В кн.: Бём
[1975], с. 122—146.

Фенстад (ред.) (Fenstad J. Е. (ed.))

[1971] Proceedings of the Second Scandinavian Logic Symposium. Stu-
dies in Logic 63, North-Holland, Amsterdam.
Феферман (Feferman S.)

[1975] A language and axioms for explicit mathematics. В кн.: Кроссли
[1975], с. 87—139.

[1980] Constructive theories of functions and classes. В кн.: Бофйа и
др. [1980], с. 159-224.

[1982] Towards useful type-free theories I. Preprint, Dept. Mathematics

Stanford, Ca 94305 USA.
Фитч (Fitch F. B.)

[1974] Elements of combinatory Logic. Yale University Press, New Ha-
ven and London.

[1980] An extension of a system of combinatory logic. В кн.: Хиндли
Селдин [1980], с. 125—140.

Фогель (Vogel H.)

[1976] Ein Starker Normalisationssatz fur die Bar-rekursiven Funktio-

nale. Arch. Math. Lolgik 18, pp. 81—84.
Фолькен (Volken H.)

[1978] Formale Stetigkeit und Modelle des Lambda-Kalkuls. Disserta-
tion. Eidgen. Technische Hochschule, Zurich.
Форчун и др. (Fortune S. et al. == Fortune S., Leivant D., O'Donnell M.)

[1980] The expressiveness of simple and second order type structures
Research Report RC8542, IBM Research Center   York-town
Heights, NY 10598, USA.
Фреге (Frege G.)

[1893/1903] Grundgesetze der Arithmetik, begriffschriftlich abgeleitel

Jena; reprint: Olms, Hildesheim, 1962.
Фридман (Friedman H.)

[1975] Equality between functionals. В кн.: Парих [1975] с 22—37
Хайланд (Hyland J. M. E.)                                       '

[1973] A simple proof of the Church— Rosser theorem. Typescript, Ox-
ford University, 7 pp.
[1975] Recursion Theory on the Countable Functionals. Dissertation

Oxford University.
[1975a] A survey of some useful partial order relations on terms of the

lambda calculus. В кн.: Бём [1975], с. 83—95.
[1976] A syntactic characterization of the equality in some models of

the X-calculus, J. London Math. Soc. (2), 12 pp 361—370
Халмош (Halmos P. R.)

[1960] Naive Set Theory. D. van Nostran, Princeton.
Ханатани (Hanatani Y.)

[1966]  Calculabilite des fonctionnels recursives primitives de type fini siir

les nombres  naturels. Ann. Japan. Ass. Philos. Sci 3, pp 19—30
Харари fHarary F.)

[1969] Graph Theory. Addison-Wesley, Reading, MA, 3rd Ed. 1977
Хелман (Helman G.)

[1977] Restricted Lambda-abstraction and Interpretation of Some Non-
classical Logics. Dissertation, University of Pittsburgh.

Литература                          585

Хината (Hinata S.)

[1967]  Calculability of primitive recursive functionals of finite type.

Science Reports of the Tokyo Kyoiku Daigaku, A, 9, pp. 218—

235.
Хиндли (Hindley J. R.)

[1964] The Church—Rosser Property and a Result in Combinatory Lo-
gic. Dissertation, University of Newcastle-upon-Tyne.
[1967] Axioms for strong reduction in combinatory Logic. J. Symbolic

Logic 32, pp. 224—236.
[1969]  The principal type scheme of an object in combinatory logic.

Trans. Amer. Math. Soc. 146, pp. 29—60.
[1977] Combinatory reductions and lambda-reductions compared. Z.

Math, Logik Grundlag. Math. 23, pp. 169—180.
[1978] Reductions of residuals are finite. Trans. Amer. Math. Soc. 240,

pp. 345—361.
[1982] The simple semantics for Coppo—Dezani—Salle type assygn-

ment. В кн.: Дедзани, Монтанари [1982], с. 212—226.
[1983] The completness for typing lambda terms. Theor. Comput. Sci.

22 (to appear).

Хиндли и др. (Hindley J. R. et al. = Hindley J. R., Lercher В., Seldin J. P.)
[1972] Introduction to Combinatory Logic. Cambridge University Press,

London.
Хиндли, Лонго (Hindley J. R., Longo G.)

[1980] Lambda calculus models and extensionality. Z. Math. Logik

Grundl Math. 26, pp. 289—310.
Хиндли, Селдин (ред.) (Hindley J. R., Seldin J. P. (eds.))

[1980] To H. B. Curry: Essays on Combinatory Logic, Lambda-Calcu-
lus and Formalism. Academic Press, New York and London.
Цукер (Zuker J.)

[1975] Formalization of classical mathematics in Automath. В кн.:

Гийом [1977], с. 135—145.
Чёрч (Church A.)

[1932/3] A set of postulates for the foundation of logic. Annals of Math.

(2) 33, pp. 346—366 and 34, pp. 839—864,
[1936] An unsolvable problem of elementary number theory. Amer. J.

Math. 58, pp. 354—363.
[1936a] A note on the Entscheidungsproblem. A correction. J. Symbolic

Logic 1, pp. 40—41, 101—102.
[1937] Combinatory logic as a semigroup (abstract). Bull. Amer. Math.

. Soc. 43, p.p. 333.
[1941] The Calculi of Lambda Conversion. Princeton University Press,

Princeton.
[1956] Introduction to Mathematical Logic. Princeton University Press

Princeton. [Имеется перевод: Чёрч А. Введение в математиче-
скую логику.—M.: ИЛ, I960.]
Чёрч, Клини (Church A., Kleene S. С.)

[1937] Formal definitions in the theory of ordinal numbers. Fund. Math.

28, pp. 11—21.
Чёрч, Poccep (Church A., Rosser J. B.)

[1936] Some properties of conversion. Trans. Amer. Math. Soc. 39,

pp. 472—482.
Швихтенберг (Schwichtenberg H.)

[1975]  Elimination of higher type levels in definitions of primitive re-
cursive functions by means of transfinite recursion. В кн.: Роуз,

Шепердсон [1975], с. 279—303.
[1975/6] Definierbare funktionen in ?i-Kalkiil mit Typen. Arch. Math.

Logic Grunlagenforsch. 17, (3—4), pp. 113—114.
[1982] Complexity of normalization in the pure typed lambda calculus.

В кн.: Трулстра, ван Дален [1982], с. 453—458.

586 Литература

Шейнфннкель М. И.

[1924] Ober die Bausteine der mathernatischen Logik. Math. Annalen 92

pp. 305—316.
Шенфилд (Schoenfield J. R.)

[1967] Mathematical Logic. Addison-Wesley, Reading, Ma. [Имеется
перевод: Шенфплд Дж. Математическая логика.—М.: Наука
1975,]
Шовен (Chauvin A.)

[1979] Theory of objects and set theory: introduction and semantics.

Notre Dame J. Formal Logic 20, pp. 37—54.
Шроэр (Schroer D E.)

[1965]  The Church—Rosser Theorem. Dissertation, Cornell University

Ithaca NY.
Энгелер (Engeler E.)

[1981] Algebras and combinators. Algebra Universalis, no. 3, pp. 389—

392.  •
Эндертон (Enderton H. В.)

[1972] A Mathematical Introduction to Logic. Academic Press, New

York and London.
Юэ (Huet G.)

[1977] Confluent reductions: abstract properties and applications to term
rewriting systems. 18-th IEEE Symposium on Foundations of
Computer Science, pp. 30—45,
Юэ, Оппен (Huet G., Oppen С.)

[1980] Equations and rewrite rules, a survey. Technical Reoort

CSL—111, SRI International.
Якопини (Jacopini G.)

[1975] A condition for identifying two elements of whatever model of
combinatory logic. В кн.: Бём [1975], с. 213—219.

Предметный указатель

алгебраическое п.ч.у. м. 28
а. н. ф. см. аппроксимативная нор-
мальная форма
аппликативная структура 101

— — экстенсиональная 93, 101
аппроксимативная нормальная форма

366
аппроксимация 366

базис 172

бесконечная ^-нормальная форма 241
бесконечное т^-расширение 238
бесконечный терм 558

— •п-редукт 237
блок 265

— оригинальный 104, 246

вкладывается 104, 246

внутренность 110

вхождение 37

выворачивание по Бёму 249, 252

выталкивание на бесконечность 230

генератор 176

— универсальный 177
г. н. ф. см. головная нормальная фор-
ма
головная нормальная форма 52, 180

— — — главная 184

— — — с оригинальной головой 251

— — — Х-свободная 251

— переменная 180

— редукция 180
головной редекс 180
гомоморфизм 104, 106
готовое множество 255
готовый терм 251
граф (редукционный) 67
группа алгебры 525

— комбинаторная 526

— рекурсивная 540

двойственная функция 513
декартово замкнутая категория 119
.— произведение 119

деке (-часть) 340
дерево 205

— Бёма см. дерево бёмовское

— бёмовского типа 226

— бёмовское 58, 221

— лежащее в основе 220, 224

— Накадзимы 504

— помеченное 220

— похожее на V-дерево 233

— частично помеченное 224

— эффективное бёмовское 225
диаграмма 308

— расщепляющаяся 307

— элементарная 307
дискретное множество 268
дискриминатор 511
длина редукционной цепочки 328

— терма 35
дно 22

замкнутость относительно аппликации
207

— — композиции 144, 186

— — минимизации 144, 186

— — правила 91

— — примитивной рекурсии 144, 186

— — равенства 151

— — — комбинаторов 152
замкнутый терм 36
замыкание 36, 335

— рефлексивное 62

— совместимое 62

— транзитивное 62

изоморфизм 104
иллативная комбинаторная логика 47,

561

индексирование 491
индикатор переменных 232
интерпретация 101, 114
истинностные значения 141, 195
K(Pi) -исчисление 35
Щ3)т1-исчисление 43
U(p)-исчисление 48
V(P)^-исчисление 49

588 Предметный указатель

?Л(Р)- исчислен не 35
ДК(Р)т]-исчисление 43

каноническое отображение 94
категория декартово замкнутая 119

— — — строго конкретная 124
квазилевая редукция 188
квази-ОЛ'-редукц!1я 333
когерентное п. ч. у. м. 30
код конечной последовательности 11

— — — (не) обеспеченный 459
комбинатор 36

— неподвижной точки 54, 140

— — — бёмовский 150

— собственный 191
комбинаторная алгебра 92, 103

— — экстенсиональная 93

— группа 526

— логика 47, 56, 158

— модель 129

— — устойчивая 129

— полнота 42, 102

— полугруппа 136, 525
комбинаторные аксиомы 107, 167
коммутирующие отношения 75
компактный элемент 28
композиция 142
В-конверсия 35
Tl-конверсия 43
конвертируемость 35, 63
конечность разверток 292
контекст 41

— кратно нумерованный 374
критическая последовательность 210

левый редекс 187
лемма о генеричности 373

— — кубе 317

— Хиндли — Розена 76

локально представимое отображение

135, 513
локальный К 215

магическая тройка 461
мальцевское многообразие 94
метка 220, 224
модель из замкнутых термов 93, 109

— — открытых термов 93, 109

— — термов 93, 109

— вторая Клини 218

— первая Клини 218
мультиблок 266
мультимножество 310

направленное множество 22
наследственно    не-О-уииверсальиыи

генератор 447
находится левее 187

независимое множество 420
непротиворечивая теория 44
неразрешимый терм 52, 178
несравнимые термы 45
не-0-терм 447
нормальная форма 45, 64

— — аппроксимативная 366

— — бесконечная 241

— — головная 52, 180
В-нормальная форма 45
рт]-нормальная форма 45
нумерованное множество 156

— — позитивное 523

— — полное 523

— — предполное 157

н. ф. см. нормальная форма

обеспеченное число 459
область (значений) 509
оболочка Каруби 125
операция замыкания 384
^.-определимая функция 50, 51, 186
V-определимая функция 195
определимое отображение 509
оригинальное множество 261
осмысленная ^.-теория 410
остаток 286

отделимое множество 258, 260
/-отделимое множество 264
^"-отделимое множество 430
откладывание б-редукции 405

— т]-редукции 386

— Й-редукции 84, 391

— г\- и 0-редукцин 392
отношение конгруэнтности 61

— равенства 61

— редукции 62

— совместимое 61

отображение алгебраическое 103

— определимое 509

— представнмое 103, 509
оценка 101

парадоксальный комбинатор 141
переменная 34, 565

— свободная 36, 565

— связанная 36, 565
перестановка конечная наследствен
ная 137, 533

— наследственная 137, 533
перестановщик 251
перечисление 173

п. о. см. полуосмысленная теория
поддерево 205, 227
подстановка 39

подстановочпое отношение 66
подстановщик 495
подструктура 104

589

Предметный указатель

подтерм 37

— активный 37

— пассивный 37

— подчеркнутый 445

— соответствующий 448

— точно подчеркнутый 448
подчеркнутый C/.-терм 436

— ^-терм 445

подъем 286, 309, 360

полезный узел 260-

полная решетка 22

полное нумерованное множество 523

— частично упорядоченное множе-
ство 22
полнота комбинаторная 42, 102

— по Гильберту — Посту 95

— редукций изнутри 364
полугруппа комбинаторная 525

— модели 525

полуосмысленная теория 20, 429
полупрямое произведение 539
понятие редукции 62
порожденное множество 172
правило свертывания 64

— слабой экстенсиональности 44

— термов 91

— ext 91, 161

— S 91
го-правило 91

— Париха 462

превосходит 246

предиаграмма 309

представимое отображение 103, 509

преобразование 250

— бёмовское 250, 264

— разрешающее 250, 264
приличная теория 515
примитивно рекурсивные функциона-
лы 555

причина пометки 375
проверка на нуль 143, 148
проективный предел 27, 540

— — рекурсивный 137, 540
проектирование 286, 309, 360
проекции 119
проекция 471

противоречивая теория 44
п. ч. у. м. 22

— — — — алгебраическое 28

— _ — — когерентное 30

равенство (отношение) 62
равенство (формула) 44

— замкнутое 44

равномерная последовательность 57,

175, 514

равномерно рекурсивная система 540
развертка 79, 288

— полная 288

различимое множесгво 261

— — нормальное 265
разрежение редукции 320
разрешимый терм 52, 57, 70, 178
/-разрешимый терм 194
/(-разрешимый терм 194
У-разрешимый терм 430
расширение 131, 236, 237, 238
ре (-часть) 340
регулярное множество 271
редекс 64

— внутренний 299

— головной 180

— зацикливающий 346

— левый 187

— обеспеченный 319

— пустой 305

— сворачиваемый 319

— специальный 340, 344

/-редекс 80, 297

Я-редекс 297

редукт 63

редукции сильно эквивалентные 314

— слабо эквивалентные 304

— //-эквивалентные 304
редукционная диаграмма 80

— стратегия 81, 327

— — частичная 335

— цепочка 66
редукция 66

— внутренняя 299

— головная 180

— изнутри 364

— квазиголовная 352

— квазилевая 188

— левая 328

— не затрагивающая множества 370

— одношаговая 305

— пустая 66

— сильная 161

— слабая 161

— собственная 66

— стандартная 80, 298
В-редукция 63
Bri-редукция 75
о-редукция 399
ri-редукция 63
О-редукция 63
редуцируется 63
рекурсивные функции 145
ретракт 28
ретракция 28

рефлексивное п. ч. у. м. 116
решетка алгебраическая 30

— непрерывная 30

— полная 22
ромба свойство 65

— — слабое 69

р. п. = рекурсивно перечислимое

590 Предметный указатель

свертка 64

свертывания правило 64

свойство области 509

селектор 251

семейство 177

сильно нормализуемое отношение 68

— нормализуемый терм 68

— эквивалентные редукции 314
скелет терма 352
слабая экстенсиональность 44
слабое свойство ромба 69

— — Чёрча — Россера 69
совместное подмножество 30
согласованные множества термов 255

— наборы термов и переменных 42

— термы 255

соглашение о переменных 38

спаривание 142

— сюръективное 142, 554
спаривающая функция см. спарива-
ние

спектр терма 351
специальное множество 266
стандартизация 320
стратегия 326

— Гросса—Кнута 331

— зацикливающая 327

— кофинальная 327

— левой редукции 328

— нормализующая 327

— одношаговая 326

— рекурсивная 326

— скелетная 352

— со свойством Чёрча — Россера 327

— эффективная 326

— В- (1) -оптимальная 328

— (1)-оптимальная 328

теорема аппроксимации 492, 498

— непрерывности 372

— нормализации 329

— об области значений 435

— — устойчивости 378

— о двойной неподвижной точке 149

— — конечности разверток 292, 316

— — консервативности 345

— — кратной неподвижной точке 149

— — неподвижной точке 36, 55

— — — — бесконечная 191

— — — — вторая 151

— — — — для п. ч. у. м. 26

— — последовательности вычислений
377

— — рекурсии

— — сильной нормализации 359 (для
помеченной редукции), 556 (для
гёделевской системы У}

— — стандартизации 301

теорема Скотта 434

— характеризации 497, 500

— Чёрча — Россера 74 (для 6), 78
(для Рп), 162 (для CL), 284 (че-
рез лемму о полосе), 294 (через
конечность разверток), 316 (силь-
ная форма), 360 (через помеченную
редукцию), 395 (для р(г1)П)

теория непротиворечивая 44

— полная по Гильберту — Посту 95

— существенно неразрешимая 153
терм абстракционный 179

— аппликационный 179

— безымянный 567

— замкнутый 36

— легкий 402

— минимальный 334

— над аппликативной структурой 101

— перечисляющий множество 173

— Плоткина 453

— помеченный 353

— порядка 0 444

— похожий на переменную 447

— производный 340

— свободноголовый 528

— типа 1 529

— типа сг 549

— ^-бесконечный 68

— У-легкий 432

— У-обратимый 528
термы конгруэнтные 38

— порожденные множеством 172
тип 548

— основной 548

типовая комбинаторная логика 549

— структура комбинаторная 551

— — экстенсиональная 551
типовое ^-исчисление 549
топология Виссера 433

— гиперсвязная 433

— деревьев 59, 136, 234, 518

— Скотта 22

точное преобразование 255

удовлетворять правилу 112
узел дерева 205

— — виртуальный 241
универсальный генератор 177
условное выражение 142
устойчивый элемент 131

формальное обращение 536
формулы-типы 559
функтор декартов 127
функция алгебраическая 103

— исходная 144

— представимая 103

— предшествования 143

— следования 148

Предметный указатель                     591

функция числовая частичная 185

— ^-определимая 50, 51, 186

цикл 335
цифровая система 55, 147

— — адекватная 148

— — нормальная 148
цифры 54, 143, 195

— стандартные 148

— Чёрча 195

частный случай 250

— — свободноголовый 528
Чёрча — Россера свойство 65

— — теорема см. теорема Чёрча —

Россера
чистая комбинаторная логика 47

ширина F-редукционной цепочки 328

эквивалентность г. н. ф. 242

— — — — по разрешимости 388

— редукций сильная 314

— термов 242

экстенсиональная теория 91
экстенсиональность см. аппликативная

структура, комбинаторная алгебра,

^.-модель
экстенсиональный коллапс 552

В-оптимальная стратегия 328
В-1-оптимальная стратегия 328
С^-терм 158
СРО 26

CR = Чёрч -— Россер

F-(редукционная) цепочка 327

fun 466

/-базис 200

/-равномерная    последовательность

203

R-бесконечный терм 68
.t-прямой блок 266

«-конверсия 38
м-конгруэнтность 38 •
а-постоянный терм 375
й-Я-точное преобразование 255
б-символ Чёрча 400
^-алгебра 106

— богатая 136

— жесткая 110
^-модель 107

— категоричная 131

— непрерывная 134, 501

— системы У 557

— — — экстенсиональная 557
^-определимая функция 143
U-определимая функция 195
^-теория 88

— осмысленная 90, 410

— полуосмысленная 90
^,-терм 36

— замкнутый 36

— помеченный 353

V-терм 281

V-терм 48

U.-терм 365

Й-терм 447

а-модель системы У 557

Часть I. На пути к теории ...... 13

Глава 1. Введение ........•.••••••••.. 14

1.1. Аспекты ламбда-исчисления ............... 14

1.2. Полные частично упорядоченные множества и топология Скотта 21

1.3. Упражнения . .................... 31

Глава 2. Конверсия ...... ............. 34

2.1. Ламбда-термы и конверсия ............... 34

2.2. Некоторые варианты теории ). ............. 46

2.3. Обзор части II .................... 64

2.4. Упражнения . .................... bf>

Глава 3. Редукция ....... ............. 61

3.1. Понятие редукции ................... 61

3.2. Бета-редукция . ................... 70

3.3. Г)-редукция . .................... 75

3.4. Обзор части III .................... 79

3.5. Упражнения ...................... 85

Глава 4. Теории ...... ............... 88

4.1. Ламбда-теории . ................... 88

4.2. Обзор части IV .................... 95

4.3. Упражнения . .................... 97

Глава 5. Модели ...... ............... 99

5.1. Комбинаторные алгебры ................ 101

5.2. Ламбда-алгебры и лямбда-модели ............ 105

5.3. Синтаксические модели ................ 113

5.4. Модели в конкретных декартово замкнутых категориях . . . .116

5.5. Модели в произвольных декартово замкнутых категориях . . .119

I 5.6. Другие описания моделей. Категоричные модели ....... 127

! 5.7. Обзор части V .................... 133

5.8. Упражнения . .................... 138

4acib ii. 1\инис1д-:ня ........

Глава 6 Классическое ламбда-исчисление .... ....

6.1. Комбинаторы неподвижной точки .............

6.2. Стандартные комбинаторы ...............

6.3. Ламбда-определимость . ................

6.4. Цифровые системы ..................

6.5. Еще о неподвижных точках; гёделевские номера .......

6.6. Результаты о неразрешимости ..............

6.7. Отступление: рефлексивные предложения и теорема о рекурсии

6.8. Упражнения    ....................

Глава 7. Теория комбинаторов ..... .........

7.1. Комбинаторная логика   ................

7.2. Редукция для CL ...................

7.3. Соотношение между CL и t. ...............

7.4. Упражнения . ....................

Глава 8. Классическое ламбда-исчисление (продолжение)

8.1. Базисы и перечисления .................

82. Равномерность; бесконечные последовательности .......

8.3. Разрешимость; головные нормальные формы ........

8.4. Ламбда-определимость частичных функций .........

8.5. Упражнения . ....................

Глава 9. U-исчисление . . , . . ............

9.1. Общие соображения ..................

9.2. Определимость . ...................

9.3. Комбинаторы ............ .........

9.4 Разрешимость .  ...................

9.5. Упражнения . ....................

Глава 10. Деревья Бёма ...... ...........

10.1. Основные факты ...................

10.2. Сравнение деревьев Бёма. Топология деревьев на Л .....

10.3. Техника выворачивания по Бёму ........ ....

10.4. Отделимость термов .................

10.5. Отделимость в ^/-исчислении ..............

10.6. Упражнения .....................

Часть III. Редукция ........

Глава 11. Фундаментальные теоремы ..... . . . . .

11.1. Теорема Чёрча—Россера ...............

11.2. Конечность разверток .................

11.3. Теорема о консервативности для V ...........

11.4. Стандартизация . ..................

11.5. Упражнения ....................

Глава 12. Сильно эквивалентные редукции .... • . . •

12.1. Редукционные диаграммы ...............

12.2. Сильные варианты теорем CR и FDI ...........

12.3. Сильный вариант теоремы стандартизации .........

12.4. Упражнения ,.,,,,,.. ............

иелиыление

Глава 13. Редукционные стратегии ...... ......

13.1. Классификация стратегий ...............

13.2. Эффективные нормализующие и кофинальные стратегии . . .

13.3. Рекурсивная CR-стратегия ...............

13.4. Эффективная зацикливающая стратегия ..........

13.5. Оптимальные стратегии ................

13.6. Упражнения ....,............'....

Глава 14. Помеченная редукция ...... .......

14.1. Сильная нормализация ................

14.2. Приложения .....................

14.3. Непрерывность .   ..................

14.4. Последовательность вычислений и устойчивость .......

14.5. Упражнения .....................

Глава 15. Другие понятия редукции .... .......

15.1. prj-редукция   ....................

15.2. рт]й-редукцня . ................'...

15.3. Дельта-редукция ...................

15.4. Упражнения .....................

Часть IV. Теории .........

Глава 16. Осмысленные теории ....... .......

16.1. Теория Эё  .............

16.2. Теория Уё* ..............'.'..'.'.'.'.

16.3. 2tt° осмысленных теорий ..........

16.4. Теория д5  .................. ^ '. '.

16.5. Упражнения ...............'...'..

Глава 17. Другие ламбда-теории ..... ........

17.1. Полуосмысленные и р. п. теории ............

17.2. Омега-теории . ...........'....'.'..'.

17.3. Частичная корректность ш-правила в 'kv\ ..........

17.4. ш-правило и теория Sev\ ................

17.5. Упражнения .....................

Часть V. Модели .........

Глава 18. Построение моделей ...... ........

18.1. Графиковая модель Рш ......

18.2. Модель До.   ........           '    ••••••

18.3. Модель и  ..........,.'. '. '.'.'.'.'.''

18.4. Упражнения . ........'....

Глава 19. Локальная структура моделей ... .....

19.1. Локальная структура модели Рш .........

19.2. Локальная структура модели Doo ........

19.3. Непрерывные ^-модели .......'.... '. '. ' '

19.4. Упражнения ............ '.

Глава 20. Глобальная структура моделей .... • . . .

20.1. Экстенсиональность, категоричность

20.2. Свойство области  ••••-..... 1 ...''

20.3. Результаты о неопределимости ...........

20.4. Локальная и глобальная представимость .......

20.5. Топология деревьев на моделях ...........

20.6. Упражнения ...................

Глава 21. Комбинаторные группы ..... . . . . .

21.1. Комбинаторные полугруппы ............

21.2. Характеризация обратимости ............

21.3. Группы G(^) и G(3S*} ..............

21.4. Упражнения ... ................

Приложения ........

Приложение А. Типовое ламбда-исчисление . . . • •

A.I. Чистое типовое ламбда-исчисление ..........

А.2. Примитивно рекурсивные функционалы ........

А.З. Формулы-типы . .................

Приложение В. Иллативная комбинаторная логика • .

Приложение С. Переменные ......

Заключительные упражнения ............