*** MK: the list constructor with a better semantics *** |

## Syntax

In this section we extend *terms*, as defined in Section Positive Conditions, with *lists* formalized as sequences.

### Sequences

The alphabet of the language is extended with the symbols `Seq` and `|`, and the language of positive conditions in Section Symbols and Signatures is extended with list terms, essentially sequences.

***TBD: In BLD/Syntax, permit polyadic signature for |

**Sequence terms.** A sequence term has one of these forms:

A

is of the form**non-extended sequence**`Seq(t`_{1}...`t`_{m}`)`, where`t`_{1}, ...,`t`_{m}are terms.An

is of the form**extended sequence**`Seq(t`_{1}...`t`_{n}`|``t)`, where n>0 and`t`_{1}, ...,`t`_{n},`t`are terms.

For `m=0`, the non-extended sequence `Seq( )` is called the * empty sequence*.

### EBNF for the Presentation Syntax

We now extend the presentation syntax of Positive Conditions to a presentation syntax for sequences.

EBNF grammar TERM ::= Const | Var | Uniterm | LIST LIST ::= 'Seq(' TERM* ')' | 'Seq(' TERM+ ` | ` TERM ')'

For example, three Prolog lists can be represented as follows.

Example 1 (presentation syntax of empty, non-extended, and extended lists) Prolog: a. [] b. [a,Y,c] c. [a,Y,c|Z] RIF: a. Seq( ) b. Seq(a ?Y c) c. Seq(a ?Y c | ?Z)

### XML Syntax

The following is an XML-serializing mapping of the presentation syntax in Section EBNF for the Presentation Syntax, extending the one in Section Positive Conditions.

Classes, roles and their intended meaning - Seq (sequence) - rest (rest role)

Example 2 shows the serialization of the three lists of Example 1.

Example 2 (XML syntax of empty, non-extended, and extended lists) a. <Seq/> b. <Seq> <Const>a</Const> <Var>Y</Var> <Const>c</Const> </Seq> c. <Seq> <Const>a</Const> <Var>Y</Var> <Const>c</Const> <rest><Var>Z</Var></rest> </Seq>

Lists can be decomposed, e.g. in conditions using explicit equality as shown in Example 3.

Example 3 (List equality) a. Presentation syntax: Seq(Head | Tail) = Seq(a Y c) b. XML syntax: <Equal> <Seq> <Var>head</Var> <rest><Var>tail</Var></rest> </Seq> <Seq> <Const>a</Const> <Var>Y</Var> <Const>c</Const> </Seq> </Equal>

This equality is true since `<Var>head</Var>` can be equated to `<Const>a</Const>` and `<Var>tail</Var>` can be equated to `<Seq><Var>Y</Var><Const>c</Const></Seq>`.

Nested lists as allowed by the grammar are illustrated in Example 4.

Example 4 (Nested list) a. Presentation syntax: Seq(a Seq(X b) c) b. XML syntax: <Seq> <Const>a</Const> <Seq> <Var>X</Var> <Const>b</Const> </Seq> <Const>c</Const> </Seq>

### Translation Between the Presentation and the XML Syntaxes

The translation from the presentation syntax to the XML syntax is given by a table, below, which extends the translation table of Positive Conditions.

Presentation Syntax | XML Syntax |
---|---|

Seq ( | <Seq> |

Seq ( | <Seq> |

## Semantics

Add the following functions to the interpretations:

**I**_{seq}:**D**^{*}→**D****I**_{tail}:**D**^{+}×→**D****D**

These functions are required to satisfy the following: **I**_{tail}(`a`_{1}, ..., `a`_{k}, **I**_{seq}(`a`_{k+1}, ..., `a`_{k+m})) = **I**_{seq}(`a`_{1}, ..., `a`_{k}, `a`_{k+1}, ..., `a`_{k+m}).

Then interpret lists as follows:

(**I**`Seq( )`) =**I**_{seq}(`<>`).Note that the domain of

**I**_{seq}is**D**^{*}, so**D**^{0}is an empty sequence of elements of, which we denote by**D**`<>`. (MK: This is what Harold's**nil**should have been.)

(**I**`Seq(t`_{1}...`t`_{n})) =**I**_{seq}((**I**`t`_{1}), ...,(**I**`t`_{n})), if`n>0`.(**I**`Seq(t`_{1}...`t`_{n}|`t`)) =**I**_{tail}((**I**`t`_{1}), ...,(**I**`t`_{n}),(**I**`t`)), if`n>0`.

*** MK: Note that this definition readily interprets malformed lists, like |