Partially defined possibly infinite lists #
This file provides a WSeq α
type representing partially defined possibly infinite lists
(referred here as weak sequences).
Weak sequences.
While the Seq
structure allows for lists which may not be finite,
a weak sequence also allows the computation of each element to
involve an indeterminate amount of computation, including possibly
an infinite loop. This is represented as a regular Seq
interspersed
with none
elements to indicate that computation is ongoing.
This model is appropriate for Haskell style lazy lists, and is closed under most interesting computation patterns on infinite lists, but conversely it is difficult to extract elements from it.
Equations
- Stream'.WSeq α = Stream'.Seq (Option α)
Instances For
Turn a sequence into a weak sequence
Equations
- Stream'.WSeq.ofSeq = (fun (x1 : α → Option α) (x2 : Stream'.Seq α) => x1 <$> x2) some
Instances For
Equations
- Stream'.WSeq.coeSeq = { coe := Stream'.WSeq.ofSeq }
Equations
- Stream'.WSeq.coeList = { coe := Stream'.WSeq.ofList }
Equations
- Stream'.WSeq.coeStream = { coe := Stream'.WSeq.ofStream }
Equations
- Stream'.WSeq.inhabited = { default := Stream'.WSeq.nil }
Prepend an element to a weak sequence
Equations
Instances For
Compute for one tick, without producing any elements
Equations
- Stream'.WSeq.think = Stream'.Seq.cons none
Instances For
Destruct a weak sequence, to (eventually possibly) produce either
none
for nil
or some (a, s)
if an element is produced.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recursion principle for weak sequences, compare with List.recOn
.
Equations
- s.recOn h1 h2 h3 = Stream'.Seq.recOn s h1 fun (o : Option α) => Option.recOn (motive := fun (x : Option α) => (s : Stream'.Seq (Option α)) → C (Stream'.Seq.cons x s)) o h3 h2
Instances For
Equations
- Stream'.WSeq.membership = { mem := Stream'.WSeq.Mem }
Get the head of a weak sequence. This involves a possibly infinite computation.
Equations
- s.head = Computation.map (fun (x : Option (α × Stream'.WSeq α)) => Prod.fst <$> x) s.destruct
Instances For
Encode a computation yielding a weak sequence into additional
think
constructors in a weak sequence
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get the tail of a weak sequence. This doesn't need a Computation
wrapper, unlike head
, because flatten
allows us to hide this
in the construction of the weak sequence itself.
Equations
- s.tail = Stream'.WSeq.flatten ((fun (o : Option (α × Stream'.WSeq α)) => Option.recOn o Stream'.WSeq.nil Prod.snd) <$> s.destruct)
Instances For
drop the first n
elements from s
.
Instances For
Convert s
to a list (if it is finite and completes in finite time).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get the length of s
(if it is finite and completes in finite time).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Replace the n
th element of s
with a
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Remove the n
th element of s
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Map the elements of s
over f
, removing any values that yield none
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Select the elements of s
that satisfy p
.
Equations
- Stream'.WSeq.filter p = Stream'.WSeq.filterMap fun (a : α) => if p a then some a else none
Instances For
Get the first element of s
satisfying p
.
Equations
- Stream'.WSeq.find p s = (Stream'.WSeq.filter p s).head
Instances For
Zip a function over two weak sequences
Equations
- One or more equations did not get rendered due to their size.
Instances For
Zip two weak sequences into a single sequence of pairs
Equations
- Stream'.WSeq.zip = Stream'.WSeq.zipWith Prod.mk
Instances For
Get the list of indexes of elements of s
satisfying p
Equations
- Stream'.WSeq.findIndexes p s = Stream'.WSeq.filterMap (fun (x : α × ℕ) => match x with | (a, n) => if p a then some n else none) (s.zip ↑Stream'.nats)
Instances For
Get the index of the first element of s
satisfying p
Equations
- Stream'.WSeq.findIndex p s = (fun (o : Option ℕ) => o.getD 0) <$> (Stream'.WSeq.findIndexes p s).head
Instances For
Get the index of the first occurrence of a
in s
Equations
Instances For
Get the indexes of occurrences of a
in s
Equations
Instances For
union s1 s2
is a weak sequence which interleaves s1
and s2
in
some order (nondeterministically).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if s
is nil
and false
if s
has an element
Equations
- s.isEmpty = Computation.map Option.isNone s.head
Instances For
Calculate one step of computation
Equations
- s.compute = match Stream'.Seq.destruct s with | some (none, s') => s' | x => s
Instances For
Get the first n
elements of a weak sequence
Equations
- One or more equations did not get rendered due to their size.
Instances For
Split the sequence at position n
into a finite initial segment
and the weak sequence tail
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if any element of s
satisfies p
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if every element of s
satisfies p
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply a function to the elements of the sequence to produce a sequence
of partial results. (There is no scanr
because this would require
working from the end of the sequence, which may not exist.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get the weak sequence of initial segments of the input sequence
Equations
- One or more equations did not get rendered due to their size.
Instances For
Like take, but does not wait for a result. Calculates n
steps of
computation and returns the sequence computed so far
Equations
- s.collect n = List.filterMap id (Stream'.Seq.take n s)
Instances For
Map a function over a weak sequence
Equations
Instances For
Flatten a sequence of weak sequences. (Note that this allows
empty sequences, unlike Seq.join
.)
Equations
- S.join = ((fun (o : Option (Stream'.WSeq α)) => match o with | none => Stream'.Seq1.ret none | some s => (none, s)) <$> S).join
Instances For
Monadic bind operator for weak sequences
Equations
- s.bind f = (Stream'.WSeq.map f s).join
Instances For
lift a relation to a relation over weak sequences
Equations
- Stream'.WSeq.LiftRelO R C none none = True
- Stream'.WSeq.LiftRelO R C (some (a, s)) (some (b, t)) = (R a b ∧ C s t)
- Stream'.WSeq.LiftRelO R C x✝ x = False
Instances For
Definition of bisimilarity for weak sequences
Equations
- Stream'.WSeq.BisimO R = Stream'.WSeq.LiftRelO (fun (x1 x2 : α) => x1 = x2) R
Instances For
Two weak sequences are LiftRel R
related if they are either both empty,
or they are both nonempty and the heads are R
related and the tails are
LiftRel R
related. (This is a coinductive definition.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
If two sequences are equivalent, then they have the same values and
the same computational behavior (i.e. if one loops forever then so does
the other), although they may differ in the number of think
s needed to
arrive at the answer.
Equations
- Stream'.WSeq.Equiv = Stream'.WSeq.LiftRel fun (x1 x2 : α) => x1 = x2
Instances For
Equations
- Stream'.WSeq.«term_~ʷ_» = Lean.ParserDescr.trailingNode `Stream'.WSeq.«term_~ʷ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ʷ ") (Lean.ParserDescr.cat `term 51))
Instances For
auxiliary definition of tail over weak sequences
Equations
- Stream'.WSeq.tail.aux none = Computation.pure none
- Stream'.WSeq.tail.aux (some (fst, s)) = s.destruct
Instances For
auxiliary definition of drop over weak sequences
Equations
- Stream'.WSeq.drop.aux 0 = Computation.pure
- Stream'.WSeq.drop.aux n.succ = fun (a : Option (α × Stream'.WSeq α)) => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n
Instances For
Given a productive weak sequence, we can collapse all the think
s to
produce a sequence.
Instances For
The monadic return a
is a singleton list containing a
.
Equations
- Stream'.WSeq.ret a = ↑[a]
Instances For
auxiliary definition of destruct_append
over weak sequences
Equations
- Stream'.WSeq.destruct_append.aux t none = t.destruct
- Stream'.WSeq.destruct_append.aux t (some (fst, s)) = Computation.pure (some (fst, s.append t))
Instances For
auxiliary definition of destruct_join
over weak sequences
Equations
- Stream'.WSeq.destruct_join.aux none = Computation.pure none
- Stream'.WSeq.destruct_join.aux (some (s, S)) = (s.append S.join).destruct.think