编程语言理论：剑桥大学出版社(2009)

5星 · 超过95%的资源需积分: 10 22 浏览量更新于2024-07-21 1 收藏 4.12MB PDF 举报

"Theories of Programming Languages-Cambridge University Press (2009)" 《编程语言理论》是由Cambridge University Press于2009年出版的一本深入探讨编程语言理论的教科书。这本书全面而严谨地审视了编程语言设计、定义和实现的理论基础，以及用于指定和证明程序行为的系统。书中不仅涵盖了命令式编程，也涉及函数式编程，并探讨了将这些方面融合到更通用的语言中的方法。作者John C. Heynolds认识到编程语言研究的多样性背后有着统一的技术基础，他提供了一种综合性的处理方式，强调了支撑该领域基本原理的少数关键概念，如组合语义、绑定结构、域、转换系统和推理规则。这些概念构成了编程语言理论的基石。书中的基本概念及其属性用数学的严谨性来描述，但同时也通过大量的应用实例来平衡理论与实践。这些例子涵盖了程序规范和证明、并发编程、函数式编程（包括继续化和惰性求值的使用）以及类型系统。函数式编程部分详细阐述了如何利用这些技术来构造高效且易于理解的代码。书中还讨论了如何使用类型系统来确保程序的安全性和正确性，这是现代编程语言设计中的一个核心方面。类型系统可以防止类型错误，提高代码的可读性和可靠性。此外，对于并发编程的探讨，揭示了在多线程和分布式环境中的编程挑战，以及如何通过同步机制和通信模型来管理共享状态。本书不仅适合计算机科学专业的学生，也对编程语言设计师和研究人员具有很高的价值。它提供了一个全面的框架，帮助读者理解编程语言设计背后的深思熟虑和理论基础，从而能够更好地理解和创建新的编程工具和技术。总而言之，《编程语言理论》是一本深入探讨编程语言核心概念的权威之作，通过其严谨的数学表述和丰富的实例，使读者能够掌握编程语言设计的核心原理，从而在实际编程和理论研究中更加得心应手。

1.1 Abstract Syntax

Although abstract grammars have the same form as ordinary context-free

grammars, when interpreted as such they are usually highly ambiguous. Nev-

ertheless, they define an unambiguous concrete representation for phrases - one

simply uses the context-free grammar obtained by parenthesizing each nontermi-

nal on the right side of a production. (Strictly speaking, one should use paren-

theses that do not occur in the original productions or in the representations

of members of predefined sets such as (var).) The nonambiguity of this gram-

mar is insured by the parenthesization and the condition on distinct patterns.

Precedence plays no role since all of the subphrases are parenthesized.

Of course, when we write complicated phrases we will not put in all of these

parentheses, but will use certain conventions about precedence. When these con-

ventions go beyond the common usage of mathematics and most programming

languages, we will state them explicitly. A convenient device for this is a prece-

dence list, which gives the operators of the language in decreasing order of prece-

dence, with parenthesized groups having the same precedence. Such a list for

predicate logic is

(X . rem) (-unary + -binary)

< < > >)

A V

where each of the binary operators is left associative.

Rather than giving them a precedence, we will allow expressions Vv. a that

begin with a universal quantifier, or Elv. a that begin with an existential quantifier,

to follow any boolean operator, and we will assume that the body a extends to

the first stopping symbol or the end of the enclosing phrase. For predicate logic,

the only stopping symbol is an unmatched closing parenthesis. In the course

of this book, however, we will introduce several other stopping symbols (and

several other kinds of phrases that are stopped by them). Specifically, the full

set of stopping symbols is

closing delimiters, when unmatched:

) ] } : I do else fi in od of then

other stopping symbols, when unparenthesized by any delimiters:

-+ >

The other half of the story about abstract grammars is how they define an

abstract syntax that is independent of representation. Basically, while the par-

ticular patterns of terminals in productions specify a particular representation

for phrases, the rest of the grammar specifies their abstract nature. For example,

if we changed the production (intexp) ::= (intexp) - (intexp) to another, such as

(intexp) ::= div (intexp) (intexp), with the same sequence of nonterminals, we

would change the representation of the division operation without changing its

abstract character.

4 1 Predicate Logic

Actually, abstractness is lost whenever one defines phrases to be any particular

family of sets - of character strings or anything else. What is really abstract

about abstract syntax is that one can use any family of sets that satisfies certain

conditions.

First, for each nonterminal of the grammar, there must be a set of abstract

phrases, called a carrier. Thus, in the case of predicate logic, there will be three

carriers, named by the nonterminals (var), (intexp), and (assert).

Second, for each production of the abstract grammar, there must be a func-

tion among the carriers called a constructor.

Specifically, a production of the

form L ::= s0R0

... R,,,_lsn gives rise to a constructor c E Ro x .

. . x Rn_1 L.

For example, the production (intexp) ::= (intexp) = (intexp) gives rise to a con-

structor in (intexp) x (intexp) -* (intexp) that we will call c_. (Note that if we

replaced (intexp) ::= (intexp) - (intexp) by the abstractly equivalent production

(intexp) ::= div (intexp) (intexp), the nature of the constructor c- would not

change.)

In the case of predicate logic, the constructors (with arbitrary but suggestive

names) that correspond to the productions of our abstract grammar are

co, cl, C2i ... E {O} -f (intexp)

Cvar E (var) -+ (intexp)

C-canary E

(intexp) -* (intexp)

C+, C_binary

CX , C : , Crem E (intexp) x (intexp) -* (intexp)

Ctrue, Cfalse E {()} -f (assert)

C=, c#, c<, c<, c>, c> E (intexp) x (intexp) -+ (assert)

c- E (assert) -+ (assert)

CA, CV, cam, cq e (assert) x (assert) -3 (assert)

CV, C3 E (var) x (assert) -+ (assert).

(Here and throughout this book, the operator --+ is right associative and has a

lower precedence than x.)

Finally, the carriers and constructors must satisfy the following conditions:

Each constructor must be injective.

Any two constructors into the same carrier (for example, both in the first part

or both in the second part of the list that is displayed above) must have disjoint

ranges.

Every member of each carrier that is not predefined (for example, (intexp)

and (assert)) must be constructible using a finite number of applications of the

constructors.

剩余512页未读，继续阅读

jiangdmdr

粉丝: 58
资源: 766

编程语言理论：剑桥大学出版社(2009)

Foundations of Programming Languages(2nd) 无水印原版pdf

Unifying Theories of Programming - C.A.R. Hoare and He Jifeng, 1998.pdf

a Practical Theory of Programming 2015-9-19 版

unifying theories of programming

Unifying Theories of Programming and Formal Engineering Methods

Simulink 2nd Order Non-linear ODE：Discrete field Theories 2nd order non-linear ODE with Simulink-matlab开发

Scattering of Electromagnetic Waves - Theories and Applications

图像工程 Image Engineering Vol1 ,2 ,3 -Tsinghua University(2017)

Eisenhardt_1989_Building-Theories-from-Case.pdf

theories-in-junit:https的补充代码

最新资源