Coinductive formalization of unbounded computations. #
This file provides a Computation
type where Computation α
is the type of
unbounded computations returning α
.
Computation α
is the type of unbounded computations returning α
.
An element of Computation α
is an infinite sequence of Option α
such
that if f n = some a
for some n
then it is constantly some a
after that.
Instances For
pure a
is the computation that immediately terminates with result a
.
Instances For
think c
is the computation that delays for one "tick" and then performs
computation c
.
Instances For
thinkN c n
is the computation that delays for n
ticks and then performs
computation c
.
Equations
- Computation.thinkN c 0 = c
- Computation.thinkN c (Nat.succ n) = Computation.think (Computation.thinkN c n)
Instances For
runFor c n
evaluates c
for n
steps and returns the result, or none
if it did not terminate after n
steps.
Instances For
destruct c
is the destructor for Computation α
as a coinductive type.
It returns inl a
if c = pure a
and inr c'
if c = think c'
.
Instances For
run c
is an unsound meta function that runs c
to completion, possibly
resulting in an infinite loop in the VM.
Instances For
Recursion principle for computations, compare with List.recOn
.
Instances For
Bisimilarity over a sum of Computation
s
Instances For
Attribute expressing bisimilarity over two Computation
s
Instances For
Assertion that a Computation
limits to a given value
Instances For
- term : ∃ a, a ∈ s✝
assertion that there is some term
a
such that theComputation
terminates
Terminates s
asserts that the computation s
eventually terminates with some value.
Instances
Promises s a
, or s ~> a
, asserts that although the computation s
may not terminate, if it does, then the result is a
.
Instances For
Promises s a
, or s ~> a
, asserts that although the computation s
may not terminate, if it does, then the result is a
.
Instances For
length s
gets the number of steps of a terminating computation
Instances For
get s
returns the result of a terminating computation
Instances For
Results s a n
completely characterizes a terminating computation:
it asserts that s
terminates after exactly n
steps, with result a
.
Instances For
Recursor based on membership
Instances For
Recursor based on assertion of Terminates
Instances For
Map a function on the result of a computation.
Instances For
bind over a Sum
of Computation
Instances For
bind over a function mapping α
to a Computation
Instances For
Compose two computations into a monadic bind
operation.
Instances For
Flatten a computation of computations into a single computation.
Instances For
c₁ <|> c₂
calculates c₁
and c₂
simultaneously, returning
the first one that gives a result.
Instances For
c₁ ~ c₂
asserts that c₁
and c₂
either both terminate with the same result,
or both loop forever.
Instances For
equivalence relation for computations
Instances For
LiftRel R ca cb
is a generalization of Equiv
to relations other than
equality. It asserts that if ca
terminates with a
, then cb
terminates with
some b
such that R a b
, and if cb
terminates with b
then ca
terminates
with some a
such that R a b
.
Instances For
Alternate definition of LiftRel
over relations between Computation
s