Assignment 1; 28-May-2001

Practical Semantics; Summer 2001

Harold Boley; DFKI, Univ. Kaiserslautern

There is the following simple 1-to-1 correspondence between the natural numbers from 0 and the flat lists over nil (informally, "suc[" corresponds to "cns[nil,"):
number notation:                     list notation:
decimal   suc(cessor) constructor    c(o)ns constructor                square brackets
0         0                          nil                               nil
1         suc[0]                     cns[nil,nil]                      [nil]
2         suc[suc[0]]                cns[nil,cns[nil,nil]]             [nil,nil]
3         suc[suc[suc[0]]]           cns[nil,cns[nil,cns[nil,nil]]]    [nil,nil,nil]
...       . . .                      . . .                             ...
a) An instantiated antecedent of Peano's induction principle ( http://www.ltn.lv/~podnieks/gt3.html  ), nat(0) and (for all N) nat(N) => nat(suc[N]), can be written as Prolog/Relfun-like Horn clauses (facts and rules) using the above unary suc and binary cns constructor notations thus ( all sources at http://www.dfki.uni-kl.de/~boley/pracsem/assignment1.rfp  ):
       nat(0).                           flat(nil).
       nat(suc[N]) :- nat(N).            flat(cns[nil,F]) :- flat(F).
Their (infinite) Herbrand models are {nat(0), nat(suc[0]), ...} and , 1-to-1, {flat(nil), flat(cns[nil,nil]), ...}. Show that nat(suc[suc[0]]) is a 'theorem'; same for flat(cns[nil,cns[nil,nil]]).  Hints (alternative): (i) Bottom-up method: Starting from the Horn facts, use the Horn rules to generate the Herbrand models (e.g. with paper and pencil) up to those 'ground' (variablefree) theorems. (ii) Top-down method: Starting from those theorems, use the Horn rules to reduce them (e.g. with Prolog or Relfun) to the Horn facts.

b)  A unary even relation can be defined for the natural numbers as follows:

       even(0).
       even(suc[suc[N]]) :- even(N).
Its (infinite) Herbrand model is {even(0), even(suc[suc[0]]), ...}. Transfer this definition and Herbrand model to flat lists.

c) A binary less relation can be defined for the natural numbers as follows:

       less(0,suc[N]).
       less(suc[M],suc[N]) :- less(M,N).
Its (infinite) Herbrand model is {less(0,suc[0]), ..., less(suc[0],suc[suc[0]]), ..., . . .}.  (i) Transfer this definition and Herbrand model to flat lists. (ii) Write binary equal relations for natural numbers and flat lists generating the Herbrand models {equal(0,0), equal(suc[0],suc[0]), ...} and , 1-to-1, {equal(nil,nil), equal(cns[nil,nil],cns[nil,nil]), ...}, respectively.  Hint: Consider using equal variable names instead of recursion.

d) A ternary add relation can be defined for the natural numbers as follows, where the first two arguments are viewed as 'inputs' and the third as 'output', like in add(suc[suc[0]],suc[suc[suc[0]]],Z):

       add(0,N,N).
       add(suc[M],N,suc[R]) :- add(M,N,R).
Transfer this definition to an app relation over flat lists, where app(end) 'concatenates' two lists into a third one. What happens with add and app if you use (e.g. in Prolog or Relfun) their first argument as 'output' and their second and third arguments as 'inputs', like in add(X,suc[suc[suc[0]]],suc[suc[suc[suc[suc[0]]]]])?

e) How could one define a length (number of elements) relation for flat lists? What happens if you invert the roles of 'input' and 'output'? Consider the following Horn rule:

       flattiny(F) :- flat(F), length(F,N), less(N,suc[suc[suc[suc[suc[0]]]]]).
Describe in one sentence what is defined by it. How many elements of the form flattiny(F) does the (infinite) Herbrand model of the joined flattiny, flat, length, and less definitions contain? Could the flattiny definition be shortened or simplified? What changes when length is defined as a unary function instead as a binary relation?

f) Generalize your list definitions in b) to e) from the flat lists over nil to the flat lists over the natural numbers from 0. How could one define the nested lists over nil and the nested lists over the natural numbers from 0?

g) Give an XML markup for the definitions of a) in RFML (e.g. using Relfun) or in RuleML.