Stuck on assignment

Using the Model Assembler code from Topic 4, give an Operational Semantics definition

for Java’s switch statement? Briefly explain your why your definition provides the

requested Operational Semantics.

3. Using the Denotational Semantics addition example given in this Topic as a guide, look

up in Wikipedia “Lambda Calculus” the Lambda Calculus expressions for true, false,

and logical-And. Create the Lambda Calculus denotation (expression) for the following

syntactic expression:

⟦true && false⟧

4. Using Axiomatic Semantics, prove the statements in Question 6 and 7 are not equivalent

unless the two operands are equal. Again, be precise with a formal proof.

5. Java’s indexOf(int ch) returns the first occurrence of the character in the character

sequence represented by corresponding String object, or -1 if the character doesn’t occur

in the String. Using Axiomatic Semantics, give formal pre- and post-conditions for this

indexOf method.

Following the formal type system introduced in the Simply Typed Lambda Calculus

Primer in this Topic, add pair data structure term to the language. For example, we’ll

use the Haskell notation of parentheses to represent our pair data structure in the

Lambda Calculus. We’ll use a Java like notation of a “.” to represent the first (fst) and

second (snd) functions. Hence, in an Applied Calculus with Boolean and Natural

Number types, we might have,

(true, 1)

(true, 1).fst ⇒ true

(true, 1).snd ⇒ 1

a. Give the new syntax and value extensions (Table 1 and 3)

b. Give the new evaluation rules (Table 2). Hints: you’ll need to give two rules

capturing the direct implementations of the fst and snd. You’ll need to give four

more rules capturing what it means to take a reduction step for the terms used in

the fst and snd functions. Consider rules for a fully evaluated pair and partially

evaluated pairs. Here’s the last and most difficult the needed six rules:

𝑡2 → 𝑡2

′

{𝑣1,𝑡2

} → {𝑣1,𝑡2

′

}

To further assist you, here’s an evaluation (pay attention to the order this

evaluation/reduction takes place since the evaluation rules must force this

ordering (i.e. it’s like the discussion of the call-by-name vs. value associated with

the Beta-reduction rule in this Topic’s notes.

{succ 4, if false then true else false}.fst

⇒ {5, if false then true else false}.fst

⇒ {5, false}.fst

⇒ 5

c. Give the new typing rules (Table 4). Hint, a 2-tuple is a binary relation, whose

value types can be represented with a cartesan-product 𝑇1 × 𝑇2 Hint: type the

evaluation rules that form a pair, fst, and snd.

Using your typing rules with an assumed Applied Lambda Calculus. Give proofs (these

are very short) of the types of the previous two examples. That is,

a. Given (true, 1) prove that (true, 1).fst results in a Boolean type and (true 1).snd

results in a Natural Number type

b. Given {succ 4, if false then true else false}.fst, prove this results in a Natural

Number type.