ProgrammingLanguagesandLogicsLectureNotes(CornellCS4110)资源-CSDN文库

Cornell

需积分: 10 186 浏览量 2017-03-08 15:59:06 上传评论收藏 2.46MB PDF 举报

资源详情

资源评论

CS 4110 – Programming Languages and Logics

Lecture #2: Introduction to Semantics

What is the meaning of a program? When we write a program, we represent it using sequences of

characters. But these strings are just concrete syntax—they do not tell us what the program actually

means. It is tempting to deﬁne meaning by executing programs—either using an interpreter or

a compiler. But interpreters and compilers often have bugs! We could look in a speciﬁcation

manual. But such manuals typically only offer an informal description of language constructs.

A better way to deﬁne meaning is to develop a formal, mathematical deﬁnition of the seman-

tics of the language. This approach is unambiguous, concise, and—most importantly—it makes

it possible to develop rigorous proofs about properties of interest. The main drawback is that the

semantics itself can be quite complicated, especially if one attempts to model all of the features of

a full-blown modern programming language.

There are three pedigreed ways of deﬁning the meaning, or semantics, of a language:

• Operational semantics deﬁnes meaning in terms of execution on an abstract machine.

• Denotational semantics deﬁnes meaning in terms of mathematical objects such as functions.

• Axiomatic semantics deﬁnes meaning in terms of logical formulas satisﬁed during execution.

Each of these approaches has advantages and disadvantages in terms of how mathematically so-

phisticated they are, how easy they are to use in proofs, and how easy it is to use them to imple-

ment an interpreter or compiler. We will discuss these tradeoffs later in this course.

1 Arithmetic Expressions

To understand some of the key concepts of semantics, let us consider a very simple language

of integer arithmetic expressions with variable assignment. A program in this language is an

expression; executing a program means evaluating the expression to an integer. To describe the

syntactic structure of this language we will use variables that range over the following domains:

x, y, z ∈ Var

n, m ∈ Int

e ∈ Exp

Var is the set of program variables (e.g., foo, bar , baz , i , etc.). Int is the set of constant integers

(e.g., 42, 40, 7). Exp is the domain of expressions, which we specify using a BNF (Backus-Naur

Form) grammar:

e ::= x

| n

| e

+ e

| e

* e

| x := e

; e

Mul(Int 2, Add(Var "foo", Int 1))

We could express the same structure in a language like Java using a class hierarchy, although it

would be a little more complicated:

abstract class Expr { }

class Var extends Expr { String name; .. }

class Int extends Expr { int val; ... }

class Add extends Expr { Expr exp1, exp2; ... }

class Mul extends Expr { Expr exp1, exp2; ... }

class Assgn extends Expr { String var, Expr exp1, exp2; .. }

2 Operational semantics

We have an intuitive notion of what expressions mean. For example, the 7 + (4 * 2) evaluates to 15,

and i := 6 + 1 ; 2 * 3 * i evaluates to 42. In this section, we will formalize this intuition precisely.

An operational semantics describes how a program executes on an abstract machine. A small-step

operational semantics describes how such an execution proceeds in terms of successive reductions—

here, of an expression—until we reach a value that represents the result of the computation. The

state of the abstract machine is often referred to as a conﬁguration. For our language a conﬁguration

must include two pieces of information:

• a store (also known as environment or state), which maps integer values to variables. Dur-

ing program execution, we will refer to the store to determine the values associated with

variables, and also update the store to reect assignment of new values to variables,

• the expression to evaluate.

We will represent stores as partial functions from Var to Int and conﬁgurations as pairs of expres-

sions and stores:

Store ≜ Var ⇀ Int

Conﬁg ≜ Store × Exp

We will denote conﬁgurations using angle brackets. For instance, ⟨σ, (foo + 2) * (bar + 2)⟩ is a con-

ﬁguration where σ is a store and (foo + 2) * (bar + 2) is an expression that uses two variables, foo

and bar . The small-step operational semantics for our language is a relation →⊆ Conﬁg ×Conﬁg

that describes how one conﬁguration transitions to a new conﬁguration. That is, the relation →

shows us how to evaluate programs one step at a time. We use inﬁx notation for the relation →.

That is, given any two conﬁgurations ⟨σ

, e

⟩ and ⟨σ

, e

⟩, if (⟨e

, σ

⟩, ⟨e

, σ

⟩) is in the relation →,

then we write ⟨σ

, e

⟩ → ⟨σ

, e

⟩. For example, we have ⟨σ, (4 + 2) * y⟩ → ⟨σ, 6 * y⟩. That is, we can

evaluate the conﬁguration ⟨σ, (4 + 2) * y⟩ one step to get the conﬁguration ⟨σ, 6 * y⟩.

Using this approach, deﬁning the semantics of the language boils down to to deﬁning the

relation → that describes the transitions between conﬁgurations.

One issue here is that the domain of integers is inﬁnite, as is the domain of expressions. There-

fore, there is an inﬁnite number of possible machine conﬁgurations, and an inﬁnite number of

possible single-step transitions. We need a ﬁnite way of describing an inﬁnite set of possible tran-

sitions. We can compactly describe → using inference rules:

n = σ(x)

⟨σ, x ⟩ → ⟨σ, n⟩

VAR

⟨σ, e

⟩ → ⟨σ

′

, e

′

⟩

⟨σ, e

+ e

⟩ → ⟨σ

′

, e

′

+ e

⟩

LADD

⟨σ, e

⟩ → ⟨σ

′

, e

′

⟩

⟨σ, n + e

⟩ → ⟨σ

′

, n + e

′

⟩

RADD

p = m + n

⟨σ, n + m⟩ → ⟨σ, p⟩

ADD

⟨σ, e

⟩ → ⟨σ

′

, e

′

⟩

⟨σ, e

* e

⟩ → ⟨σ

′

, e

′

* e

⟩

LMUL

⟨σ, e

⟩ → ⟨σ

′

, e

′

⟩

⟨σ, n * e

⟩ → ⟨σ

′

, n * e

′

⟩

RMUL

p = m × n

⟨σ, m * n⟩ → ⟨σ, p⟩

MUL

⟨σ, e

⟩ → ⟨σ

′

, e

′

⟩

⟨σ, x := e

; e

⟩ → ⟨σ

′

, x := e

′

; e

⟩

ASSGN1

′

= σ[x 7→ n]

⟨σ, x := n ; e

⟩ → ⟨σ

′

, e

⟩

ASSGN

The meaning of an inference rule is that if the facts above the line holds, then the fact below the

line holds. The fact above the line are called premises; the fact below the line is called the conclusion.

The rules without premises are axioms; and the rules with premises are inductive rules. We use the

notation σ[x 7→ n] for the store that maps the variable x to integer n, and maps every other variable

to whatever σ maps it to. More explicitly, if f is the function σ[x 7→ n], then we have

f(y) =

{

n if y = x

σ(y) otherwise

3 Using the Semantics

Now let’s see how we can use these rules. Suppose we want to evaluate the expression (foo + 2) * (bar + 1)

with a store σ where σ(foo) = 4 and σ(bar) = 3. That is, we want to ﬁnd the transition for the

conﬁguration ⟨σ, (foo + 2) * (bar + 1)⟩. For this, we look for a rule with this form of a conﬁguration

in the conclusion. By inspecting the rules, we ﬁnd that the only rule that matches the form of

our conﬁguration is LMUL, where e

= foo + 2 and e

= bar + 1 but e

′

is not yet known. We can

instantiate LMUL, replacing the metavariables e

and e

with appropriate expressions.

⟨σ, foo + 2⟩ → ⟨e

′

, σ⟩

⟨σ, (foo + 2) * (bar + 1)⟩ → ⟨σ, e

′

* (bar + 1)⟩

LMUL

Now we need to show that the premise actually holds and ﬁnd out what e

′

is. We look for a rule

whose conclusion matches ⟨σ, foo + 2⟩ → ⟨e

′

, σ⟩. We ﬁnd that LADD is the only matching rule:

⟨σ, foo⟩ → ⟨σ, e

′′

⟩

⟨σ, foo + 2⟩ → ⟨σ, e

′′

+ 2⟩

LADD

We repeat this reasoning for ⟨σ, foo⟩ → ⟨σ, e

′′

⟩ and ﬁnd that the only applicable rule is the axiom

VAR:

σ(foo) = 4

⟨σ, foo⟩ → ⟨σ, 4⟩

VAR

剩余110页未读，继续阅读

评论收藏

内容反馈

Programming Languages and Logics Lecture Notes (Cornell CS4110)

评论0

最新资源

Programming Languages and Logics Lecture Notes (Cornell CS4110)

评论0

最新资源

相关推荐

编程语言语义学讲义Lecture Notes on Semantics of Programming Languages

Programming Languages Lecture Notes (Washington CSE341)

Transition to OO Programming Lecture Notes (Cornell CS1130)

Programming Languages Lecture Notes (NEU CS4400)

Data Structures and Functional Programming Lecture Notes (Cornell CS3110)

Practical Foundations for Programming Languages

A Novel Combination of Answer Set Programming with Description Logics

Practical.Foundations.for.Programming.Languages.2nd

Foundations of Programming Languages Lecture Notes (CMU 15-312)

Logics for Computer Science

Temporal Logics in Computer Science

QUANTUM LOGICS

Some Recent Results in Metric Temporal Logics

LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems

Springer - Ontology Learning and Population from Text

Logics in Artificial Intelligence

神经网络Mccullotch pitt matlab代码：神经网络Mccullotch pitt matlab代码or and and not logics-matlab开发

handbook of spatial logics

Kripke’s Worlds_ An Introduction to Modal Logics via Tableaux

proof theory for fuzzy logics

Temporal Description Logics

Probability Logics

A NEW INTRODUCTION TO MODAL LOGIC

Vector Davinci官方帮助配置使用手册（AutoSAR）.pdf

c++入门，核心，提高讲义笔记

离散数学及其应用 第八版 奇数编号练习答案.pdf

数字图像处理 冈萨雷斯 课后习题

科研伦理与学术规范 期末考试2 （40题）.pdf

离散数学及其应用第八版奇数编号练习答案.pdf

数字图像处理冈萨雷斯课后习题

科研伦理与学术规范期末考试2 （40题）.pdf