Foundations of Programming Languages Lecture Notes (CMU 15-312)
3星 · 超过75%的资源 需积分: 9 96 浏览量
2017-03-08
16:02:29
上传
评论
收藏 2.71MB PDF 举报 
Lecture Notes on Inductive Definitions
15-312: Foundations of Programming Languages
Frank Pfenning
Lecture 2
September 2, 2004
These supplementary notes review the notion of an inductive definition
and give some examples of rule induction. References to Robert Harper’s
draft book on Programming Languages: Theory and Practice are given in square
brackets, by chapter or section.
Given our general goal to define and reason about programming lan-
guages, we will have to deal with a variety of description tasks. The first is
to describe the grammar of a language. The second is to describe its static
semantics, usually via some typing rules. The third is to describe its dy-
namic semantics, often via transitions of an abstract machine. On the sur-
face, these appear like very different formalisms (grammars, typing rules,
abstract machines) but it turns out that they can all be viewed as special
cases of inductive definitions [Ch. 1]. Following standard practice, inductive
definitions will be presented via judgments and inference rules providing
evidence for judgments.
The first observation is that context-free grammars can be rewritten in
the form of inference rules [Ch. 3.2]. The basic judgment has the form
s A
where s is a string and A is a non-terminal. This should be read as the
judgment that s is a string of syntactic category A.
As a simple example we consider the language of properly matched
parentheses over the alphabet Σ = {(, )}. This language can be defined by
the grammar
M : : = ε | (M ) | M M
with the only non-terminal M. Recall that ε stands for the empty string.
Rewritten as inference rules we have:
LECTURE NOTES SEPTEMBER 2, 2004
剩余209页未读，继续阅读
资源评论
blue123dfg2017-10-12还不错的资源
