Q: Why bother doing proofs about programming languages? They are almost always boring if the definitions are right.
A: The definitions are almost always wrong. (查看原文)
n one end of the spec- trum are powerful frameworks such as Hoare logic, algebraic specification languages, modal logics, and denotational semantics. These can be used to express very general correctness properties but are often cumbersome to use and demand a good deal of sophistication on the part of programmers. (查看原文)
At the other end are techniques of much more modest power—modest enough that automatic checkers can be built into compilers, linkers, or program analyzers (查看原文)
The more abstract focuses on connections between various “pure typed lambda-calculi” and varieties of logic, via the Curry-Howard correspondence (查看原文)
The mathemati- cal foundations of inductive reasoning will be considered in more detail in Chapter 21, where we will see that all these specific induction principles are instances of a single deeper idea. (查看原文)
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, ... (查看原文)
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 ... (查看原文)
In languages in the ML family, for example, every datatype definition implicitly introduces a recursive type. Each use of one of the constructors to build a value of the datatype implicitly includes a fold, and each constructor appearing in a pattern match implicitly forces an unfold. Similarly, in Java each class definition implicitly introduces a recursive type, and invoking a method on an object involves an implicit unfold. This felicitous overlap of mechanisms makes the iso-recursive style quite palatable in practice. (查看原文)
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). (查看原文)
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. (查看原文)
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 ℷ_:Unit.t, called a thunk. This “thunked form” of t is a syntactic value; all the computation involved in evaluating t is postponed until the thunk is applied to unit. (查看原文)
