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.

return a is the computation that immediately terminates with result a.

think c is the computation that delays for one "tick" and then performs computation c.

thinkN c n is the computation that delays for n ticks and then performs computation c.

head c is the first step of computation, either some a if c = return a or none if c = think c'.

tail c is the remainder of computation, either c if c = return a or c' if c = think c'.

empty α is the computation that never returns, an infinite sequence of thinks.

run_for c n evaluates c for n steps and returns the result, or none if it did not terminate after n steps.

destruct c is the destructor for computation α as a coinductive type. It returns inl a if c = return a and inr c' if c = think c'.

run c is an unsound meta function that runs c to completion, possibly resulting in an infinite loop in the VM.

corec f b is the corecursor for computation α as a coinductive type. If f b = inl a then corec f b = return a, and if f b = inl b' then corec f b = think (corec f b').

left map of ⊕

right map of ⊕

terminates s asserts that the computation s eventually terminates with some value.

promises s a, or s ~> a, asserts that although the computation s may not terminate, if it does, then the result is a.

length s gets the number of steps of a terminating computation

get s returns the result of a terminating computation

results s a n completely characterizes a terminating computation: it asserts that s terminates after exactly n steps, with result a.

Map a function on the result of a computation.

Compose two computations into a monadic bind operation.

Flatten a computation of computations into a single computation.

c₁ <|> c₂ calculates c₁ and c₂ simultaneously, returning the first one that gives a result.

c₁ ~ c₂ asserts that c₁ and c₂ either both terminate with the same result, or both loop forever.

lift_rel 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.