# 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).
`       flattiny(F) :- flat(F), length(F,N), less(N,suc[suc[suc[suc[suc[0]]]]]).`