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]

... . . . . . . ...

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.