A.1.3 Sequences

Syntax

<>, <1,2,3>	sequence literals
<m..n>	closed range (from integer m to n inclusive)
<m..>	open range (from integer m upwards)
s^t	sequence catenation
#s, length(s)	length of a sequence
null(s)	test if a sequence is empty
head(s)	give first element of a non-empty sequence
tail(s)	give all but the first element of a non-empty sequence
concat(s)	join together a sequence of sequences
elem(x,s)	test if an element occurs in a sequence
<x1,... xn | x<-s, b>	comprehension

Equivalences

null(s) ≡	s==<>
<m..n> ≡	if m<=n then <m>^<m+1..n> else <>
elem(x,s) ≡	not null(< z | z <-s, z==x >
< x | > ≡	< x >
< x | b, ...> ≡	if b then < x | ...> else <>
< x | x'<-s, ...> ≡	concat(< < x | ...> | x'<-s >)

Remarks

All the elements of a sequence must have the same type. concat and elem behave as if defined by

concat(s) = if null(s) then <> else head(s)^concat(tail(s)) elem(_, <>) = false elem(e, <x>^s) = e==x or elem(e,s)

Similarly, we can define palindrome to test if a sequence is its own reverse (that is `s == reverse(s)') by

palindrome(<x>^s^<y>) = x==y and palindrome(s) palindrome(_) = true