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

Figure 9-1: Pure simply typed lambda-calculus (→)

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, then Γ ⊢ t1 : Bool and Γ ⊢ t2, t3 : R .

9.3.3 Theorem [Uniqueness of Types]:

In a given typing context , a term t (with free variables all in the domain of ) has at most one type. That is, if a term is typable, then its type is unique. Moreover, there is just one derivation of this typing built from the inference rules that generate the typing relation.

9.3.4 Lemma [Canonical Forms]:

1. If v is a value of type Bool, then v is either true or false.

2. If v is a value of type T1→T2, then v = λx:T1.t2.

9.3.5 Theorem [Progress]:

Suppose t is a closed, well-typed term (that is, ⊢ t : T for some T). Then either t is a value or else there is some t' with t → t'.

Proof: Straightforward induction on typing derivations. The cases for boolean constants and conditions are exactly the same as in the proof of progress for typed arithmetic expressions (8.3.2). The variable case cannot occur (because t is closed). The abstraction case is immediate, since abstractions are values. The only interesting case is the one for application, where t = t1 t2 with ⊢ t1 : T11→T12 and ⊢ t2 : T11. By the induction hypothesis, either t1 is a value or else it can make a step of evaluation, and likewise t2. If t1 can take a step, then rule E-App1 applies to t. If t1 is a value and t2 can take a step, then rule E-App2 applies. Finally, if both t1 and t2 are values, then the canonical forms lemma tells us that t1 has the form λx:T11.t12, and so rule E-AppAbs applies to t.

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

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 it. For example, consider the term

which we can write more readably as id (id (z. id z)). This term contains three redexes:

Under full beta-reduction, we might choose, for example, to begin with the innermost redex, then do the one in the middle, then the outermost:

● Under the normal order strategy, the leftmost, outermost redex is always reduced first. Under this strategy, the term above would be reduced as follows:

Under this strategy (and the ones below), the evaluation relation is actually a partial function: each term t evaluates in one step to at most one term t'.

● The call by name strategy is yet more restrictive, allowing no reductions inside abstractions. Starting from the same term, we would perform the first two reductions as under normal-order, but then stop before the last and regard z. id z as a normal form:

Variants of call by name have been used in some well-known programming languages, notably Algol-60 (Naur et al., 1963) and Haskell (Hudak et al., 1992). Haskell actually uses an optimized version known as call by need (Wadsworth, 1971; Ariola et al., 1995) that, instead of re-evaluating an argument each time it is used, overwrites all occurrences of the argument with its value the first time it is evaluated, avoiding the need for subsequent re-evaluation. This strategy demands that we maintain some sharing in the run-time representation of terms—in effect, it is a reduction relation on abstract syntax graphs, rather than syntax trees.

● Most languages use a call by value strategy, in which only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value—a term that is finished computing and cannot be reduced any further.5 Under this strategy, our example term reduces as follows:

The call-by-value strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, non-strict (or lazy) strategies such as call-by-name and call-by-need evaluate only the arguments that are actually used.

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

Definition [Terms, by inference rules]: The set of terms is defined by the following rules:

inference 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 satisfying these rules is often (as here) not stated explicitly.

Two points of terminology deserve mention. First, rules with no premises (like the first three above) are often called axioms. In this book, the term inference rule is used generically to include both axioms and “proper rules” with one or more premises. Axioms are usually written with no bar, since there is nothing to go above it. Second, to be completely pedantic, what we are calling “inference rules” are actually rule schemas, since their premises and conclusions may include metavariables. Formally, each schema represents the infinite set of concrete rules that can be obtained by replacing each metavariable consistently by all phrases from the appropriate syntactic category—i.e., in the rules above, replacing each t by every possible term.

Finally, here is yet another definition of the same set of terms in a slightly different, more “concrete” style that gives an explicit procedure for generating the elements of T .

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

预序，偏序，等价关系

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 said to be a join (or least upper bound) of s and t if

s≤j and t≤j, and

for any element k ∈S with s≤k and t≤k, we have j≤k.

Similarly, an element m 2 S is said to be a meet (or greatest lower bound) of s and t if

m ≤ s and m ≤ t, and

for any element n ∈S with n ≤ s and n ≤ t, we have n ≤m.

良基关系
在数学中，类 X 上的一个二元关系 R 被称为是良基的，当且仅当所有 X 的非空子集都有一个 R-极小元

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

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 that, when given an index, always returns 0.

To look up an element of an array, we simply apply the function to the desired index.

The interesting part of the encoding is the update function. It takes an array, an index, and a new value to be stored at that index, and does its job by creating (and storing in the reference) a new function that, when it is asked for the value at this very index, returns the new value that was given to update, and on all other indices passes the lookup to the function that was previously stored in the reference.

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

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 evidence has a strongly computational feel. For example, a proof of a proposition P ⊂ Q can be viewed as a mechanical procedure that, given a proof of P, constructs a proof of Q—or, if you like, a proof of Q abstracted on a proof of P. Similarly, a proof of P ^ Q consists of a proof of P together with a proof of Q. This observation gives rise to the following correspondence:
Logic Programming languages
---------------------------------------------------------------
propositions types
proposition P ⊃ Q type P⟼Q
proposition P ^ Q type P × Q
proof of proposition P term t of type P
proposition P is provable type P is inhabited

龙三 (の日常)

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

龙三 (の日常)

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

龙三 (の日常)

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

龙三 (の日常)

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

龙三 (の日常)

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

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

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

龙三 (の日常)

2019-07-09 23:10

龙三 (の日常)

2019-07-09 22:52

龙三 (の日常)

2019-06-24 21:48

龙三 (の日常)

2018-06-21 22:04