### Types and Programming Languages (15) 更多

• ##### 第287页
This lemma is reminiscent of the traditional technique for establishing redundancy of the transitivity rule in inference systems, often called “cutelimination proofs” (see §16.1). The condition ...
• ##### 第277页
In a system with iso-recursive types, we introduce, for each recursive type μX.T, a pair of functions that “witness the isomorphism” by mapping values back and forth between the two types: ... I...
• ##### 第239页
Using dummy lambda-abstractions to control evaluation order is a wellknown trick in the functional programming community. The idea is that an arbitrary expression t can be turned into a function ...
里氏替换原则
• ##### 第159页
The typing rules for ref, :=, and ! follow straightforwardly from the behaviors we have given them.
• ##### 第158页
A reference cell need not contain just a number: the primitives above allow us to create references to values of any type, including functions. For example, we can use references to functions to gi...
• ##### 第104页
9.3.1 Lemma [Inversion of the typing relation]: 1. If Γ ⊢ x : R, then x:R ∈ Γ . 2. If Γ ⊢ λx:T1. t2 : R, then R = T1!R2 for some R2 with Γ , x:T1 ⊢ t2 : R2. 3. If Γ ⊢ t1 t2 : R, ...
• ##### 第56页
Several different evaluation strategies for the lambda-calculus have been studied over the years by programming language designers and theorists. Each strategy defines which redex or redexes in a t...
• ##### 第27页
Definition [Terms, by inference rules]: The set of terms is defined by the following rules: The first three rules here restate the first clause of Definition 3.2.1; the next four capture clauses (2...
• ##### 第18页
预序，偏序，等价关系 A reflexive and transitive relation R on a set S is called a preorder on S. A reflexive, transitive, and anti-symmetric relation R is called a partial order on S. A reflexive, ...
• ##### 第108页
The "⟼" type constructor comes with typing rules of two kinds: 1. an introduction rule (T-Abs) describing how elements of the type can be created, and 2. an elimination rule (T-App) describing h...
• ##### 第56页
in Lambda-Calculus: * 应用序（applicative order）先求值参数而后应用 * 正则序（normal order）完全展开而后归约 * 传名调用（call by name）不允许在 abstraction 里规约，lazy * 传值调用（call by value...

### 无政府、国家和乌托邦 (1)

• ##### 第4页
英国唯物主义哲学家和政治思想家霍布斯假设了一个自然状态，他认为在国家成立以前，人类生活在一种自然状态中。在自然状态下，人们具有同等的自然权利，不仅是平等的，而且每个人又都是自由的，但人们趋利避害的...

TSS 描述符：
LDT 描述符：
调用门：
段选择子
存储器的段描述符格式：

### Topology Without Tears (2)

• ##### 第191页
There are three important ways of creating new topological spaces from old ones. They are by forming “subspaces”, “quotient spaces”, and “product spaces”:
<前页 1 2 3 4 5 6 7 8 9 10