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.