# Types and Programming Languages的笔记(11)

## 按有用程度按页码先后最新笔记

• ### 展开 收起 第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, then there is some type T11 such that Γ ⊢ t1 : T11→R and Γ ⊢ t2 : T11. 4. If Γ ⊢ true : R, then R = Bool. 5. If Γ ⊢ false : R, then R = Bool. 6. If Γ ⊢ if t1 then t2 else t3 : R, ...

2019-06-30 14:41   1人喜欢

• ### 展开 收起 第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 term can fire on the next step of evaluation. ● Under full beta-reduction, any redex may be reduced at any time. At each step we pick some redex, anywhere inside the term we are evaluating, and reduce...

2019-06-22 18:55   1人喜欢

• ### 展开 收起 第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) and (3). Each rule is read, “If we have established the statements in the premise(s) listed above the line, then we may derive the conclusion below the line.” The fact that T is the smallest set s...

2019-06-18 11:01   1人喜欢

• ### 展开 收起 第34页

龙三 (の日常)

2019-06-17 18:55   1人喜欢

• ### 展开 收起 第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, transitive, and symmetric relation on a set S is called an equivalence on S. 最小上确界，最大下确界 Suppose that ≤ is a partial order on a set S and s and t are elements of S. An element j 2 S is sai...

2019-06-15 19:13   1人喜欢

• ### 展开 收起 第88页

中小型文化叙事 (当代舶来品研究)

2013-07-21 19:03   1人喜欢

• ### 展开 收起 第159页

龙三 (の日常)

The typing rules for ref, :=, and ! follow straightforwardly from the behaviors we have given them.

2019-07-09 23:10

• ### 展开 收起 第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 give a (not very efficient) implementation of arrays of numbers, as follows. Write NatArray for the type Ref (Nat → Nat). To build a new array, we allocate a reference cell and fill it with a function ...

2019-07-09 22:52

龙三 (の日常)

• ### 展开 收起 第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 how elements of the type can be used. Briefly, the idea is that, in constructive logics, a proof of a proposition P consists of concrete evidence for P. What Curry and Howard noticed was that such evid...

2018-06-21 22:04

<前页 1 2 