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.
pure a
is the computation that immediately terminates with result a
.
Equations
- Computation.pure a = { val := Stream'.const (some a), property := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.const (some a) x = some x_1 → Stream'.const (some a) x = some x_1) }
Equations
- Computation.instCoeTCComputation = { coe := Computation.pure }
think c
is the computation that delays for one "tick" and then performs
computation c
.
Equations
- Computation.think c = { val := Stream'.cons none ↑c, property := (_ : ∀ (n : ℕ) (a : α), Stream'.cons none (↑c) n = some a → Stream'.cons none (↑c) (n + 1) = some a) }
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)
head c
is the first step of computation, either some a
if c = pure a
or none
if c = think c'
.
Equations
tail c
is the remainder of computation, either c
if c = pure a
or c'
if c = think c'
.
Equations
- Computation.tail c = { val := Stream'.tail ↑c, property := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.tail (↑c) x = some x_1 → ↑c (x + 1 + 1) = some x_1) }
empty α
is the computation that never returns, an infinite sequence of
think
s.
Equations
- Computation.empty α = { val := Stream'.const none, property := (_ : ∀ (x : ℕ) (x_1 : α), Stream'.const none x = some x_1 → Stream'.const none x = some x_1) }
Equations
- Computation.instInhabitedComputation = { default := Computation.empty α }
run_for c n
evaluates c
for n
steps and returns the result, or none
if it did not terminate after n
steps.
Equations
- Computation.runFor = Subtype.val
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'
.
Equations
- Computation.destruct c = match ↑c 0 with | none => Sum.inr (Computation.tail c) | some a => Sum.inl a
run c
is an unsound meta function that runs c
to completion, possibly
resulting in an infinite loop in the VM.
Equations
- Computation.run x = let c := x; match Computation.destruct c with | Sum.inl a => a | Sum.inr ca => Computation.run ca
Recursion principle for computations, compare with List.recOn
.
Equations
- One or more equations did not get rendered due to their size.
Corecursor constructor for corec
corec f b
is the corecursor for Computation α
as a coinductive type.
If f b = inl a
then corec f b = pure a
, and if f b = inl b'
then
corec f b = think (corec f b')
.
Equations
- One or more equations did not get rendered due to their size.
Bisimilarity over a sum of Computation
s
Attribute expressing bisimilarity over two Computation
s
Equations
- Computation.IsBisimulation R = ∀ ⦃s₁ s₂ : Computation α⦄, R s₁ s₂ → Computation.BisimO R (Computation.destruct s₁) (Computation.destruct s₂)
Assertion that a Computation
limits to a given value
Equations
- Computation.Mem a s = (some a ∈ ↑s)
Equations
- Computation.instMembershipComputation = { mem := Computation.Mem }
assertion that there is some term
a
such that theComputation
terminatesterm : ∃ a, a ∈ s
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
.
Equations
- Computation.Promises s a = ∀ ⦃a' : α⦄, a' ∈ s → a = a'
Promises s a
, or s ~> a
, asserts that although the computation s
may not terminate, if it does, then the result is a
.
Equations
- One or more equations did not get rendered due to their size.
length s
gets the number of steps of a terminating computation
Equations
- Computation.length s = Nat.find (_ : ∃ n, Option.isSome (↑s n) = true)
get s
returns the result of a terminating computation
Equations
- Computation.get s = Option.get (↑s (Nat.find (_ : ∃ n, Option.isSome (↑s n) = true))) (_ : Option.isSome (↑s (Nat.find (_ : ∃ n, Option.isSome (↑s n) = true))) = true)
Results s a n
completely characterizes a terminating computation:
it asserts that s
terminates after exactly n
steps, with result a
.
Equations
- Computation.Results s a n = ∃ h, Computation.length s = n
Recursor based on memberhip
Equations
- One or more equations did not get rendered due to their size.
Recursor based on assertion of Terminates
Equations
- Computation.terminatesRecOn s h1 h2 = Computation.memRecOn (_ : Computation.get s ∈ s) (h1 (Computation.get s)) h2
Map a function on the result of a computation.
Equations
- One or more equations did not get rendered due to their size.
bind over a Sum
of Computation
bind over a function mapping α
to a Computation
Equations
- One or more equations did not get rendered due to their size.
Compose two computations into a monadic bind
operation.
Equations
- Computation.bind c f = Computation.corec (Computation.Bind.f f) (Sum.inl c)
Equations
- Computation.instBindComputation = { bind := @Computation.bind }
Flatten a computation of computations into a single computation.
Equations
- Computation.join c = c >>= id
c₁ <|> c₂
calculates c₁
and c₂
simultaneously, returning
the first one that gives a result.
Equations
- One or more equations did not get rendered due to their size.
c₁ ~ c₂
asserts that c₁
and c₂
either both terminate with the same result,
or both loop forever.
Equations
- Computation.Equiv c₁ c₂ = ∀ (a : α), a ∈ c₁ ↔ a ∈ c₂
equivalence relation for computations
Equations
- Computation.«term_~_» = Lean.ParserDescr.trailingNode `Computation.term_~_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))
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
.
Alternate defintion of LiftRel
over relations between Computation
s
Equations
- One or more equations did not get rendered due to their size.