Sequences

Funcons-beta : Sequences.cbs | PRETTY | PDF

Outline

Sequences of values
- Sequence indexing
- Homogeneous sequences

Sequences of values

[
  Funcon length
  Funcon index
  Funcon is-in
  Funcon first
  Funcon second
  Funcon third
  Funcon first-n
  Funcon drop-first-n
  Funcon reverse
  Funcon n-of
  Funcon intersperse
]

Sequences of two or more values are not themselves values, nor is the empty sequence a value. However, sequences can be provided to funcons as arguments, and returned as results. Many operations on composite values can be expressed by extracting their components as sequences, operating on the sequences, then forming the required composite values from the resulting sequences.

A sequence with elements X_1, …, X_n is written X_1,...,X_n. A sequence with a single element X is identified with (and written) X. An empty sequence is indicated by the absence of a term. Any sequence X^* can be enclosed in parentheses (X^*), e.g.: ( ), (1), (1,2,3). Superfluous commas are ignored.

The elements of a type sequence T_1,...,T_n are the value sequences V_1,...,V_n where V_1:T_1, …, V_n:T_n. The only element of the empty type sequence ( ) is the empty value sequence ( ).

(T)^N is equivalent to T,...,T with N occurrences of T. (T)^* is equivalent to the union of all (T)^N for N>=0, (T)⁺ is equivalent to the union of all (T)^N for N>=1, and (T)^? is equivalent to T | ( ). The parentheses around T above can be omitted when they are not needed for disambiguation.

(Non-trivial) sequence types are not values, so not included in types.

Meta-variables 
  T, T′ <: values

Funcon
  length(_:values^*) : =>natural-numbers

length(V^*) gives the number of elements in V^*.

Rule
  length( ) ~> 0
Rule
  length(V:values, V^*:values^*) ~> natural-successor(length(V^*))

Funcon
  is-in(_:values, _:values^*) : =>booleans
Rule
  is-in(V:values ,V′:values, V^*:values^*) ~> or(is-equal(V, V′), is-in(V, V^*))
Rule
  is-in(V:values, ( )) ~> false

Sequence indexing

Funcon
  index(_:natural-numbers, _:values^*) : =>values^?

index(N, V^*) gives the Nth element of V^*, if it exists, otherwise ( ).

Rule
  index(1, V:values, V^*:values^*) ~> V
Rule
  natural-predecessor(N) ~> N′
  -----------------------------------------------------------------
  index(N:positive-integers, _:values, V^*:values^*) ~> index(N′, V^*)
Rule
  index(0, V^*:values^*) ~> ( )
Rule
  index(_:positive-integers, ( )) ~> ( )

Total indexing funcons:

Funcon 
  first(_:T, _:values^*) : =>T
Rule
  first(V:T, V^*:values^*) ~> V

Funcon 
  second(_:values, _:T, _:values^*) : =>T
Rule
  second(_:values, V:T, V^*:values^*) ~> V

Funcon 
  third(_:values, _:values, _:T, _:values^*) : =>T
Rule
  third(_:values, _:values, V:T, V^*:values^*) ~> V

Homogeneous sequences

Funcon
  first-n(_:natural-numbers, _:(T)^*) : =>(T)^*
Rule
  first-n(0, V^*:(T)^*) ~> ( )
Rule
  natural-predecessor(N) ~> N′
  -----------------------------------------------------------------
  first-n(N:positive-integers, V:T, V^*:(T)^*) ~> (V,first-n(N′, V^*))
Rule
  first-n(N:positive-integers, ( )) ~> ( )

Funcon
  drop-first-n(_:natural-numbers, _:(T)^*) : =>(T)^*
Rule
  drop-first-n(0, V^*:(T)^*) ~> V^*
Rule
  natural-predecessor(N) ~> N′
  -----------------------------------------------------------------------
  drop-first-n(N:positive-integers, _:T, V^*:(T)^*) ~> drop-first-n(N′, V^*)
Rule
  drop-first-n(N:positive-integers, ( )) ~> ( )

Funcon
  reverse(_:(T)^*) : =>(T)^*
Rule
  reverse( ) ~> ( )
Rule
  reverse(V:T, V^*:(T)^*) ~> (reverse(V^*), V)

Funcon
  n-of(N:natural-numbers, V:T) : =>(T)^*
Rule
  n-of(0, _:T) ~> ( )
Rule
  natural-predecessor(N) ~> N′
  --------------------------------------------------
  n-of(N:positive-integers, V:T) ~> (V, n-of(N′, V))

Funcon
  intersperse(_:T′, _:(T)^*) : =>(T, (T′, T)^*)^?
Rule
  intersperse(_:T′, ( )) ~> ( )
Rule
  intersperse(_:T′, V) ~> V
Rule
  intersperse(V′:T′, V₁:T, V₂:T, V^*:(T)^*) ~> (V₁, V′, intersperse(V′, V₂, V^*))

From the PLanCompS Project

CBS-beta issues…

Suggest an improvement…

↑ →