《Types and Programming Languages》的笔记-第27页
- 章节名：Terms, by inference rules
- 页码：第27页 2019-06-18 11:01:24
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 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 .
龙三对本书的所有笔记 · · · · · ·
说明 · · · · · ·