Stenlund S. — Combinators, λ-Terms and Proof Theory :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Stenlund S. — Combinators, λ-Terms and Proof Theory

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Combinators, λ-Terms and Proof Theory

Автор: Stenlund S.

Аннотация:

The aim of this monograph is to present some of the basic ideas and results in pure combinatory logic and their applications to some topics in proof theory, and also to present some work of my own. Some of the material in chapter 1 and 3 has already appeared in my notes Introduction to Combinatory Logic. It appears here in revised form since the presentation in my notes is inaccurate in several respects.

Язык:

Рубрика: Математика/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Год издания: 1972

Количество страниц: 184

Добавлена в каталог: 29.11.2009

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

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

$s_{n}$ -terms      145
$s_{n}$ -variables      144
$\alpha$ -equality      19 28
$\beta$ -conversion      43
$\beta$ -equality      37
$\beta$ -reduction      73 74
$\beta\eta$ -conversion      43
$\beta\eta$ -reduction      45
$\beta\eta\delta$ -reduction      46 74
$\beta\eta\delta{R}$ -reduction      75
$\delta$ -redex      45
$\delta$ -reduction      45 74
$\eta$ -equality      20 33
$\forall$ -elimination      149
$\forall$ -introduction      148
$\forall$ -reduction      146
$\forall_{2}$ -reduction      146
$\lambda$ -abstraction      41
$\lambda$ -calculus      15 41
$\lambda$ -I-calculus      46
$\lambda$ -K-calculus      46
$\lambda$ -terms      41
$\omega$ -completeness      20
$\omega$ -rule      20
$\rightarrow$ -elimination      148
$\rightarrow$ -introduction      148
$\rightarrow$ -reduction      146
$\sum$ -expression      136 168
A-terms      146
Abstraction algorithm of c-terms      29
Abstraction algorithm of p-terms      26
Abstraction algorithm strong      29
Abstraction algorithm weak      29
Adjoint situation      170
Application      12
Arithmetical combinators      21
atom      27 41
Atomic $\lambda$ -terms      41
Atomic c-terms      27
Atomic combinators      27
Atomic formulas      145
Atomic types      112 146
Bachmann, H.      134
Bar-recursion      112 133
Barendregt, H.      20 52 55
Bernays, P.      87
Bound variable      41
Brouwer ordinals      112 113
C-function      172
c-model      52
Cartesian closed categories      170
Category theory      170
Church — Rosser property      32 45 73 126 156
Church — Rosser Theorem      30 45 73
Church, A.      12 15 16 46 47 67 70 73 92 107
Combination      17
Combinator      14 17 135 167
Combinator, atomic      27
Combinator, deferred      22
Combinator, pairing      94
Combinator, paradoxical      71
Combinator, primitive      20
Combinatory arithmetic      16 91
Combinatory definable      91 93
Combinatory terms      27
Completeness of the equation calculi      141 175
Completeness, combinatorial      15 55 56 64
Completeness, deductive      64
Composite product      22
composition      96
Comprehension      59
Computability      127 158
Computability function      157
Computability set      158
Computable functional      109
Computable term      127
Constant      41 113
Constant, atomic      27 41
Contraction      31 44 46 75 86 125 155
Contractum      31 44 45 75 84 86 125 155
Curry, H.B.      11 15 16 20 21 33 36 37 39 40 45 46 51 67 68 70 71 72 73 83 91 107 108 150 151
Curry’s paradox      68
Deferred combinator      22
Deferring operation      23
Definition explicit      13
Definition recursive      89
Definition theories of      89
Definitional equality      89 125 156
Dialectica interpretation      111 112 118
e-model      138
Equality      20 33 42
Equality, definitional      89 125 156
Equality, extensional      122
Equality, intensional      110 114
Equality, weak      28
Explicit definition      13
Extensionality      19 59 122
Feys, R.      15 16 21 33 36 37 39 40 45 46 51 68 71 72 73 83 108 150 151
Fitch, F.B.      21 22 67
Fixed-point theorem      102
Formula of the propositional calculus      26
Formula of the theory of species      145
Formula, atomic      145
Formula, composite      145
Fraenkel, A.      16 52
Free variable      41
Frege, G.      11 46
Function calculus      11
Function constant      144
Function in extension      12
Function in intension      12
Function spaces      53 66
Function, constructive      109
Function, continuous      53 65
Function, partial      53 97
Functional abstraction      15 28
Gentzen, G.      109 150
Girard, J.-Y.      156 157
Goedel, K.      109 110 111 117 118 119
Goodstein, R.L.      116 119
Heyting arithmetic      110 117 151
Hilbert, D.      150
Hindley, R.      37 72 73 98 107 108 123
Howard, W.      111 112 116 119 134 151

i-model      137
i-terms      144
i-variables      144
Identity combinator      17
Illative combinatory logic      16 67
Impredicativity      164 177
Induction rule      116 118
Intuitionistic analysis      112 133
Inversion principle      146
J-terms      39
Kleene, S.C.      16 46 70 91
Konstanzfunktion      14
Kreisel, G.      112 116 118 122 155
Kuratowski, C.      65 66
Lattice      53
Lawvere, W.      170
Lercher, B.      37 40
Limit spaces      65
Martin-Loef, P.      74 151 156 164
Minimalization      96
Model of the $\lambda$ -calculus      55
Model of the system of computable functionals      136
Model of the theory of combinators      52
Model of the theory of species      170
Normal form      44 45 46 125 155
Normal reduction      40
Normalizable      32 40 44 155
Numeral      114
Numeral sequence      103
One-step reduction      74 76 87
Open combination      37
p-term      25
Pairing combinator      87
Paradoxical combinator      71
Part (of term)      27
Powers      22
Prawitz, D.      112 124 143 147 151 153 155 156 164 165
Primitive recursive arithmetic      116
Proof terms      149
Quine, W.V.      21
R-constant      86
R-redex      75 84 86
R-reduction      75 86
R-system      89
R-term      86
Recursively inseparable      106
Redex in the $\lambda$ -calculus      44
Redex in the system of computable functionals      125
Redex in the theory of combinators      31
Redex in the theory of species      155
Reduction in the $\lambda$ -calculus      44
Reduction in the system of computable functionals      125
Reduction in the theory of combinators      27
Reduction in the theory of species      155
Reduction one-step      74 76 87
Reduction sequence      44
Reduction, normal      40
Reduction, strong      27 37 83
Reduction, weak      30
Regular combinator      23
Rosser, J.B.      16 36 46 51 70 73
Rule of correspondence      12
Rule of inference      114
Rule of reduction      30
Russell, B.      11 52 166
S-constant      86
Sanchis, L.E.      28 40 134
Schoenfinkel, M.      11 12 13 14 24 56 67
Schuette, K.      123
Scott, D.      53 54 55 106 107
Seldin, J.      72 108
Self-application      15 21 52
Sheffer, H.M.      11
Shoenfield, J.      97
Sn      126
Species constant      144
Species term      145
Species variable      144
Spector, C.      118 122
Standard numeral sequence      92
Stenlund, S.      28 98 123
Strong algorithm      29
Strong normal form      40
Strong Normalization Theorem      131 164
Strong reduction      27 37 83
Strongly irreducible      38
Strongly normalizable      126 155
Structure      135 165
Substitution      29 42
Subterm      27
Synonymous      89
Tait, W.W.      74 111 112 117 119 134 145 149 165 170 172
Term model      52 138 171
Term of finite type      113
Term, closed      42
Term, combinatory      27
Term, computable      127
Term, individual      144
Term, normal      44
Term, normalizable      44
Term, open      42
Term, strongly normalizable      126
Terminus      40
Theory if functionality      68
Theory of combinators      11
Theory of species      143
Troelstra, A.      117 120
Truth-functions      23 116
TYPE      112 146
Type, atomic      112 146
Type, composite      146
Type, finite      109 112
Type, higher      112
Type, infinite      59 62
U-expression      55
Uniqueness rule      123
Validity, in a structure      137 169
Verschmelzungsfunktion      14
Weak algorithm      29
Weak extensionality      122
Weak normal form      32
Weak reduction      30
Whitehead, A.N.      11
Zermelo, E.      16 52

О проекте