Plt1314 4

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

# Logistics

• Course site
• Date published: 27 Nov 2013
• Deadline SVN: 3 Dec 2013 (End of Day)
• Other logistics as previously

# Assignment

## Option 1

Invent a "strange" language and define (implement) either small or big-step semantics for it in Prolog. You could inspire yourself with examples from previous exams.

## Option 2

The semantics of arithmetic expressions is compositional, as it was discussed. This means that meaning of a compound expression is directly defined in terms of the meanings of proper subexpressions. Define a noncompositional semantics of expressions such that multiplication is defined in terms of addition and subtraction. Use the following laws:

``````0 * y = 0
1 * y = y
x * y = y + (x-1) * y for x > 0```
```

## Option 3

Define a type system (well-typedness) for the FL language. You really should extend the language upfront to include signatures for the functions. It would be rather hard to define well-typedness otherwise.

Here is again the factorial function:

``````sample(
(
[
(
factorial,
[x],
if(
binary(var(x), const(0), eq),
const(1),
binary(
var(x),
apply(
factorial,
[binary(var(x),const(1),sub)]),
mult)
)
)
],
apply(factorial, [const(5)])
)
).```
```

This is how a function with signature could look like; see "ADDED":

``````sample(
(
[
(
factorial,
integer, % ADDED FOR THE RETURN TYPE
[(x, integer)], % ADDED FOR THE ARG TYPE
if(
binary(var(x), const(0), eq),
const(1),
binary(
var(x),
apply(
factorial,
[binary(var(x),const(1),sub)]),
mult)
)
)
],
apply(factorial, [const(5)])
)
).```
```

## Option 4

### Option 4.a

Take the While language and its big-step semantics from the lecture. Disregard the while statement. Prove the following property. There are no infinite derivation trees. Write down your proof in a structured manner so that induction base, induction step, and application of the induction hypothesis are clearly recognizable.

### Option 4.b

You may instead also do this for the small-step semantics. In this case, the property reads as follows: There are no infinite derivation sequences.

page revision: 6, last edited: 27 Nov 2013 11:39