|
|
Авторизация |
|
|
Поиск по указателям |
|
|
|
|
|
|
|
|
|
|
Abramsky S., Gabbay D.M., Maibaum T.S.E. — Handbook of Logic in Computer Science: Volume 5: Logic and Algebraic Methods |
|
|
Предметный указатель |
Morphism, signature 237
Moschovakis, Y. N. 145 148 336 476 490 493 500 516 517
Moses, Y. 136
Multicategory 123
Natural number object 65
Natural number object, weak 65
Next state function 447
Noetherian 263
Non-deterministic assignment 488
Normal form 263
Normann, D. 478 493 517
NTime 140
NTIME lower bounds 166
NTIME(T(cn))-inseparable 153
NULL 57
Numbering 332
N[M/x] 44
Object 307
Object, class 307
Object, identities 307
Object, instances 307
Object, type 307
Observable sorts 298
Oles, F. 50
One-element-type 59
Only positively 145
Operation 220
Operation name 220
Operation, constant 220
Operator formula 145
Orbit 447
Order-sorted algebra 302
Order-sorted signature 301
P 88
pair 58
Papert, S. 211
Parameterization, -calculus approach 295
Parameterization, pushout approach 296
Peano arithmetic 246
Periodic points 447
persistent 238 248 274 285
Persistent, free extension 276
Poewr 138
Poigne, A. 40
Point, F. 207
Polymorphic 224
Polymorphic, lambda calculus 123
Positive and negative occurrences 144
Post's theorem 342 407 410 411—412 415 420
Pour-El, M. B. 474 476 518
PR 84
Predicate logic 241
Predicate transition 304
Prenex definition 144
Prescribed set of formulas 150
Prest, M. 207 209
Primary subtree 138
Problem 140 141
Procedures 362
Product type 57 344
Program schematology 339 489
Program scheme 489
Proj 60
Projection morphism 110
Projections of relations 348
Projective equivalence theorem 422 434—435
Proof theory 123
PROP 78
Prop-category 79
Prop-category, classifying 98
Prop-category, has equality 94
Prop-category, has existential quantification 91
Prop-category, has finite joins 83
Prop-category, has finite meets 82
Prop-category, has Heyting implications 84
Prop-category, has universal quantification 91
PSL 291
Pullback of a property 79
Pullback of an indexed type 110
Quotient algebra 226
Quotient homomorphism 226
Quotient term algebra 235
Quotient term algebra, of a set of formulas 244
Quotient term extension 275
Rabin, M. 131 142 148 184 192 193 194 195 198 207 208
Rabinovich, A. 136
Rackoff, C. 146 148 186 191 193 194 196 202 210 211
Ramakrishna, Y. 136
Random assignments 408 435—438 488
rapid prototyping 253
Rautenberg, W. 185
Reachable 231
Realizability 89
Realization 300
Reddy, U. 210
Reduct 237
Reduct and expansion 347 354 356 358
Reduct of a homomorphism 238
Reduction ordering 264
Reduction system 263
Reductions sequence 263
Register machines 484—487
Register machines, register machine with stacking 485
Register machines, register machines with counting 485
Relation symbol 77
Relations 348
Relative homomorphism 350—351
Relative while computability 375
Relativization 140
Remainder set 380
renaming 235
Representations of semantic functions 387—394
Requirement specification 253
Reset log-lin reduction 141
Rewrite ordering 264
Reyes, G. E. 81
Reynolds, J. C. 41 50 100
Richards, J. I. 474 476 518
Robertson, E. L. 184
Robinson, A. 209 210
Roman, L. 65
Rules, adjoint style 86 89
Rules, natural deduction style 85 89 93
S 88
Sacerdote, G. 207
Satisfaction 239
Satisfaction, condition 239
Satisfaction, of a judgement 117
Satisfaction, of an equation 47
Satisfaction, of sequent 82
Satisfaction, relation 239
Satisfiability problem 132
Scarpellini, B. 136 210
Scedrov, a. 123
Schmitt, P. 209
Schoening, U. 136
Scott, D. S. 41
Search 333 412—413 461
Search procedure 413
Seiferas — Fischer — Meyer Theorem 159
Seiferas, J. 159 160
Semantics, model oriented 283
Semantics, of while programs 363—364
Semantics, presentation oriented 284
Semantics, specification oriented 284
Semantics, theory oriented 284
Semenov, L. 189 210
Semicomputability equivalence theorem 431
Semicomputability with search 413—414
Sentence 144
| Sequent 78
Set 80 111
Set, -cosemidecidable 333
Set, -decidable 333
Set, -semidecidable 333
Set, clopen 451 464
Set, closed 451 464
Set, definable 408 431—435
Set, halting 324 408 414 422 428 436 457
Set, Julia 449—451
Set, open 451 464
Set, projective semicomputable 407—451
Set, recursion 493
Set, semialgebraic 444
Set, semicomputable with search 414 416 421—422
Set, while computable 324 326—329 407 409 438—451
Set, while semicomputable 324 326—329 407—451
SG 43
Shelah, S. 164 165
Shepherdson, J. C. 339 342 473 475 484 487 489 518 519
Shub, M. 438 484 506
Signature 43 101 220 322 344—360
Signature, dynamic 304
Signature, module 284
Signature, morphism 235 237
Signature, morphism, inclusion 236
Signature, order-sorted 301
Signature, strongly typed 228
Simultaneous course of values recursion 337 483
Simultaneous iterative definition 148
Slice category 111
Slobodskoi, A. M. 209
Smale, S. 438 484 506
Snapshot function 382 402 417
SND 59
sort 43 220
Sort, argument sort 220
Sort, dynamic 304
Sort, label sort 304
Sort, observable 298
Sort, target sort 220
Sound 250
Soundness 47
Specification morphism 284
Specification oriented semantics 284
Specification, adequate 252
Specification, atomic 252
Specification, design 253
Specification, e-specification 278
Specification, final 299
Specification, initial 257
Specification, language 496—500
Specification, loose 253
Specification, loose with constructors 255
Specification, requirement 253
Specification, strictly adequate 252
Split 58
Stable, coproduct 56 57
Stable, initial object 57
Stable, join 87
Stage 49
Standard signatures 351—352
Standardness assumption 353
Statement remainder function 417
Statman, R. 210
Stern, J. 191
Stirling, C. 136
Stockmeyer, L. 137 140 184 211
Stoltenberg-Hansen, V. 330 332 335 343 476 477 520
streams see "Infinite streams"
Strict N-standardness 355
Strictly adequate specification 252
Strictness condition 111
Strong monad 66
Strongly typed 228
Structural induction 362
Structure for a dependently typed theory 114
Structure for a predicate theory 80
Structure for an algebraic theory 46
Subalgebra 225 349
Subalgebra, induced 225
Subobject 80
Substitution 229
Substitution, ground 229
Substitution, theorem 230
Substitutivity condition 225
Subtype condition 302
Sufficiently complete 231
Synchronous concurrent algorithms 501
Tarski's quantifier-elimination theorem 444
Tarski, A. 79
Tautology 244
Term 227 237 349 361—364 383—387
Term, algebra 234
Term, construction 300
Term, evaluation 329 341 389—390 394—397 399—402 405 410 412 415 416 418—421 431 439 472
Term, ground 227
Term, rewriting system 264
Term, signature morphism on 237
Term, value of a 228
Term-in-context 44
Term-model 41
Terms 51
Th-algebra 47
Th-context 107
Theory 245
Theory, algebraic 45
Theory, axioms of 45
Theory, dependently typed algebraic 102
Theory, in predicate logic 77
Theory, morphism 284
Theory, oriented semantics 284
Theory, theorems of 45 78 102
Theory, translation 74
Time resource bound 140
Tiuryn, J. 136
Topos 112 122
Total object 110
Touraille, A. 208
Trakhtenbrot — Vaught Inseparability Theorem 153
Trakhtenbrot, B. A. 131 153
Transition predicate 304
TRUE 85
Tucker, J. V. 317 330 332 335 343 365 369 396 432 452 475 576 476 477 478 483 494 495 496 520 521
Turing, A. 154
TX 66
TYPE 103
Type, computation 66
Type, dependent product 120
Type, disjoint union 52
Type, empty 57
Type, function 60
Type, ground 51
Type, indexed 110
Type, inductive 62
Type, one-element 59
Type, product 57
Type-category 110
Type-category, cont classifying 107—108
Type-category, cont has dependent products 120
Type-category, cont reachable 119
Types 51
Ullman, J. D. 140 159 200
Uniform computation 324
Uniform convergence 470
Union, amalgamated 283
UNIT 60
Universality 341 387—388 399—401 439 490
Universe 243
Val 66
|
|
|
Реклама |
|
|
|