Possibly infinite lists #
This file provides a Seq α
type representing possibly infinite lists (referred here as sequences).
It is encoded as an infinite stream of options such that if f n = none
, then
f m = none
for all m ≥ n
.
Seq1 α
is the type of nonempty sequences.
Instances For
Prepend an element to a sequence
Instances For
Get the nth element of a sequence (if it exists)
Instances For
A sequence has terminated at position n
if the value at position n
equals none
.
Instances For
It is decidable whether a sequence terminates at a given position.
A sequence terminates if there is some position n
at which it has terminated.
Instances For
Get the first element of a sequence
Instances For
member definition for Seq
Instances For
If a sequence terminated at position n
, it also terminated at m ≥ n
.
If s.get? n = some aₙ
for some value aₙ
, then there is also some value aₘ
such
that s.get? = some aₘ
for m ≤ n
.
Recursion principle for sequences, compare with List.recOn
.
Instances For
Bisimilarity relation over Option
of Seq1 α
Instances For
a relation is bisimilar if it meets the BisimO
test
Instances For
Embed a list as a sequence
Instances For
Embed an infinite stream as a sequence
Instances For
Translate a sequence to a list. This function will run forever if run on an infinite sequence.
Instances For
The sequence of natural numbers some 0, some 1, ...
Instances For
Append two sequences. If s₁
is infinite, then s₁ ++ s₂ = s₁
,
otherwise it puts s₂
at the location of the nil
in s₁
.
Instances For
Map a function over a sequence.
Instances For
Flatten a sequence of sequences. (It is required that the
sequences be nonempty to ensure productivity; in the case
of an infinite sequence of nil
, the first element is never
generated.)
Instances For
Remove the first n
elements from the sequence.
Equations
- Stream'.Seq.drop s 0 = s
- Stream'.Seq.drop s (Nat.succ n) = Stream'.Seq.tail (Stream'.Seq.drop s n)
Instances For
Take the first n
elements of the sequence (producing a list)
Equations
- Stream'.Seq.take 0 x = []
- Stream'.Seq.take (Nat.succ n) x = match Stream'.Seq.destruct x with | none => [] | some (x, r) => x :: Stream'.Seq.take n r
Instances For
Split a sequence at n
, producing a finite initial segment
and an infinite tail.
Equations
- One or more equations did not get rendered due to their size.
- Stream'.Seq.splitAt 0 x = ([], x)
Instances For
Combine two sequences with a function
Instances For
Pair two sequences into a sequence of pairs
Instances For
Separate a sequence of pairs into two sequences
Instances For
Enumerate a sequence by tagging each element with its index.
Instances For
Convert a sequence which is known to terminate into a list
Instances For
Convert a sequence which is known not to terminate into a stream
Instances For
Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)
Instances For
Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).
Instances For
Convert a Seq1
to a sequence.
Instances For
Map a function on a Seq1
Instances For
Flatten a nonempty sequence of nonempty sequences
Instances For
The return
operator for the Seq1
monad,
which produces a singleton sequence.
Instances For
The bind
operator for the Seq1
monad,
which maps f
on each element of s
and appends the results together.
(Not all of s
may be evaluated, because the first few elements of s
may already produce an infinite result.)