(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.