DOC PREVIEW
U of I CS 241 - NATURAL SEMANTICS

This preview shows page 1-2-3 out of 9 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

OutlineNatural SemanticsNatural Semantics: Additional FeaturesCS421 Lecture 17: Natural Semantics1Mark [email protected] of Illinois at Urbana-ChampaignJuly 18, 20061Based on slides by Mattox Beckman, as updated by Vikram Adve, GulAgha, and Elsa GunterMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsNatural Semantics: Additional FeaturesMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesObjectivesBy the end of this lecture, you should◮be able to read and understand language definitions givenusing natural semantics◮understand some of the differences between natural andtransition semanticsMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleNatural SemanticsNatural semantics are similar to transition semantics except◮transition semantics specifies a relation between individualsteps of a computation◮while natural semantics specifies a relation between a state inthe computation and a final resultRules will be of the formhC , mi ⇓ m′And it should be the case thathC , mi →∗m′iff hC , mi ⇓ m′Mark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleAn asideBoth transition semantics and natural semantics are forms ofoperational semantics. Transition semantics is also known asstructural operational semantics, or small-step semantics. Naturalsemantics is also known as big-step semantics.Mark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleNatural Semantics of Atomic ExpressionsIn both cases we only take one step, so the semantics are roughlythe same:◮Identifiers: hX , σi ⇓ σ(X )◮Numerals: hn, σi ⇓ n◮Booleans:◮htrue, σi ⇓ true◮hfalse, σi ⇓ falseMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleArithmetic ExpressionsSince the rules for addition, subtraction, and multiplication all lookthe same except for the operator used, we will just letop = {+, −, ×} below:ha0, σi ⇓ n0ha1, σi ⇓ n1n = n0opintn1ha0op a1, σi ⇓ nMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleRelational OperationsWe again use op here to stand for a number of operations whichall have similar rules. Let op = {=, ≤} below:ha0, σi ⇓ n0ha1, σi ⇓ n1b = n0opintn1ha0op a1, σi ⇓ nMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleLogical Operations: AndSince our and operation “short-circuits”, we need two rules, onethat tells us the result when the first operation is false, and onethat tells us the result when the first operation is true:hb0, σi ⇓ falsehb0∧ b1, σi ⇓ falsehb0, σi ⇓ true hb1, σi ⇓ bhb0∧ b1, σi ⇓ bMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleLogical Operations: OrOr is similar to and – both “short-circuit”, so we also need tworules here. Note the main difference is that we flip around the valueused to decide whether to continue with the second argument:hb0, σi ⇓ truehb0∨ b1, σi ⇓ truehb0, σi ⇓ false hb1, σi ⇓ bhb0∨ b1, σi ⇓ bMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleLogical Operations: NotNegation is fairly simple – we can just handle it with two cases,one for evaluating the first argument to true, the other for false:hb, σi ⇓ falseh¬b, σi ⇓ truehb, σi ⇓ trueh¬b, σi ⇓ falseMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleCommands: SkipSimilarly to how expressions are handled, we will evaluatecommands completely, yielding the state after the command isexecuted. Skip is defined similarly to the definition in transitionsemantics:{skip, σ} ⇓ σMark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleCommands: AssignmentWith assignment, we build in the evaluation of the expressiondirectly into the assignment rule, instead of requiring two steps.ha, σi ⇓ nhX := a, σi ⇓ σ[n/X ]Mark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleCommands: SequencingSequencing again requires we completely evaluate the componentcommands. Here, we can directly see the result of the firstcommand being “passed on” to the second.hc0, σi ⇓ σ′hc1, σ′i ⇓ σ′′hc0; c1, σi ⇓ σ′′Mark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleCommands: ConditionalWe make the choice directly in the rules premises, since we arerequired to evaluate to the final state.hb, σi ⇓ true hc0, σi ⇓ σ′hif b then c0else c1, σi ⇓ σ′hb, σi ⇓ false hc1, σi ⇓ σ′hif b then c0else c1, σi ⇓ σ′Mark Hills CS421 Lecture 17: Natural SemanticsOutlineNatural SemanticsNatural Semantics: Additional FeaturesNatural SemanticsAtomic ExpressionsArithmetic ExpressionsBoolean ExpressionsCommandsExampleCommands: WhileThe rule for the while command is “recursive”, in that it refers toitself. One important point to


View Full Document

U of I CS 241 - NATURAL SEMANTICS

Documents in this Course
Process

Process

28 pages

Files

Files

37 pages

File I/O

File I/O

52 pages

C Basics

C Basics

69 pages

Memory

Memory

23 pages

Threads

Threads

14 pages

Lecture

Lecture

55 pages

C Basics

C Basics

24 pages

Signals

Signals

27 pages

Memory

Memory

45 pages

Threads

Threads

47 pages

Threads

Threads

28 pages

LECTURE

LECTURE

45 pages

Threads

Threads

30 pages

Threads

Threads

55 pages

Files

Files

37 pages

SIGNALS

SIGNALS

22 pages

Files

Files

37 pages

Threads

Threads

14 pages

Threads

Threads

13 pages

Load more
Download NATURAL SEMANTICS
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view NATURAL SEMANTICS and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view NATURAL SEMANTICS 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?