Types and Programming Languages的笔记(11)

>我来写笔记

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

  • 龙三

    龙三 (の日常)

    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人喜欢

  • 龙三

    龙三 (の日常)

    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人喜欢

  • 龙三

    龙三 (の日常)

    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人喜欢

  • 龙三

    龙三 (の日常)

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

  • 龙三

    龙三 (の日常)

    预序,偏序,等价关系 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人喜欢

  • 中小型文化叙事

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

    我为了学习haskell的类型系统来看这个书,吭哧吭哧看了7章,类型系统还没出现。满满都是泪。   (1回应)

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

  • 龙三

    龙三 (の日常)

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

    2019-07-09 23:10

  • 龙三

    龙三 (の日常)

    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

  • 龙三

    龙三 (の日常)

    2019-06-24 21:48

  • 龙三

    龙三 (の日常)

    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 后页>

笔记是你写在书页留白边上的内容;是你阅读中的批注、摘抄及随感。

笔记必须是自己所写,不欢迎转载。摘抄原文的部分应该进行特殊标明。

Types and Programming Languages

>Types and Programming Languages