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 ...
  • 第212页
  • 第186页
    里氏替换原则
  • 第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, ...
  • 第39页
  • 第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...
  • 第34页
  • 第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页
    英国唯物主义哲学家和政治思想家霍布斯假设了一个自然状态,他认为在国家成立以前,人类生活在一种自然状态中。在自然状态下,人们具有同等的自然权利,不仅是平等的,而且每个人又都是自由的,但人们趋利避害的...

x86汇编语言 (5)

Topology Without Tears (2)

  • 第203页
  • 第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 后页>