Plt1213 4

(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau

Logistics

Assignment

Both assignments are carried out within Prolog.

1. An extension of NB

Consider the following Prolog-encoded semantics and typing rules of NB:

https://slps.svn.sourceforge.net/svnroot/slps/topics/semantics/nb

Modify the type system of NB by replacing the type Nat by Int (to represent integers instead of natural numbers). Also introduce the following types: Pos (to represent the subset of Int with positive numbers), Neg (negative numbers), and Zero ("0"). That it, Pos, Neg, and Zero can be considered subtypes of Int. With negative numbers enabled, you should also revise the semantics of pred to exercise negative numbers, actually. Demonstrate the type system with examples that exercise the more specific subtypes as well as the general type Int.

2. Semantics and type system of a language for stack-based operations

Consider the following operations:

  • push i — pushes an integer literal i on the stack.
  • push b — pushes a Boolean literal b on the stack.
  • or — applies logical OR to top of stack and second top of stack, pops operands, pushes result.
  • add — applies integer ADD to top of stack and second top of stack, pops operands, pushes result.

Describe the semantics for sequences of such operations as a mapping to the resulting stack of values.

Describe a type system for sequences of such operations as a mapping to the resulting stack of types of values.

Example 1

push True
push False
or
push 42
  • Result of evaluation: [42, True]
  • Result of type checking: [Int,Bool]

Example 2

push True
push False
add
  • Result of evaluation: "your decision"
  • Result of type checking: "not well typed"