Choice trees: Nondeterministic, recursive, and impure programs in Coq | Hacker News Reader

Choice trees: Nondeterministic, recursive, and impure programs in Coq

arxiv.org

56 pointsPaulHoule8 comments

Theoretical computer science goes way over my head, but this is an interesting choice of terminology, because a branching tree of choices yet to be made is exactly how I reason about side effects in programming, whether with monads or effect handlers or something else.

So I wonder, is this new structure a generalization of existing tools, or is it something completely new?

I think a large part of the value in research like this is the rigour in implementing it as formal proofs.

Can someone ELI5 coinductive data types and cofixpoints? Also curious how they interact with the termination checker

(using a non-Coq notation and using a newer form of coinductive types)

Inductive types are built using constructors. An example, defining two lists:

l1 = nil

l2 = cons 1 l1

Induction/recursion principles (fixpoints + pattern matching) consume them to produce some other value.

Examples:

length nil = 0

length (cons x xs) = 1 + length xs

For coinductive types it's the inverse. Coinduction/corecursion principles (cofixpoints + copattern matching) produce them. Take streams with the destructors hd : Stream A -> A and tail : Stream A -> Stream A). By defining how it's destructors work on the stream, we define a stream blink : (Bool -> Stream Nat):

hd (blink True) = 0

hd (blink False) = 1

tail (blink True) = blink False

tail (blink False) = blink True

blink True is the infinite stream 0101010101010101... To consume the stream, you call the destructors on it (and receive the defined result).

Now, just like how records are inductive types defined via destructors, the same can be done allowing coinductive types to be defined via constructors. In Coq this is called positive coinductive types and they're the original form of coinductive types introduced to Coq (and the only one until ~2019), but they're also not exactly well behaved, which is why it's now recommended to use the negative form, though e.g. this paper still uses the positive form. If you want to know more about this, I'd recommend reading the Coq documentation :-)

>Also curious how they interact with the termination checker

While infinite, negative coinductive types don't pose any termination issue because they're lazy - blink only 'describes how to deconstruct it' and does not do any computation of its own. So if you apply a finite amount of destructors to it, you only get a finite computation.

(positive coinductive types are a bit more tricky - there's a special productivity condition for them.)

A tip about formatting: if you indent by 4 spaces, you get monospaced text that doesn't swallow single line breaks.

Thus:

    l1 = nil
    l2 = cons 1 l1

    length nil = 0
    length (cons x xs) = 1 + length xs

And:

    blink : Bool -> Stream Nat

    head : Stream A -> A
    head (blink True) = 0
    head (blink False) = 1

    tail : Stream A -> Stream A
    tail (blink True) = blink False
    tail (blink False) = blink True

Two spaces are sufficient.

And with https://github.com/plibither8/refined-hacker-news you get even nice gray boxes around code.

Enjoy!

In imperative code I would write it like:

    odd := {hd: 1}
    even := {hd: 0, tail: odd}
    odd.tail := even
    blink x := x ? odd : even

I guess the cofixpoint does that loop tying sort of like this?

    fix({odd, even} => {
      odd: {hd: 1, tail: even},
      even: {hd: 0, tail: odd}
    })

Is there something like a co-Y combinator to do this in pure languages?

Is the productivity condition sort of like the dual of the positivity restriction on inductive types?

To add a little bit to the other good answers:

https://wiki.c2.com/?CoinductiveDataType

Reply on news.ycombinator.com