Zulip Chat Archive

Stream: general

Topic: seq and coinduction


view this post on Zulip Kenny Lau (Mar 27 2018 at 18:23):

I see this comment in data.seq.seq:

/-
coinductive seq (α : Type u) : Type u
| nil : seq α
| cons : α → seq α → seq α
-/
 ```
Does this mean that `seq` is intended to be coinductive? Does that mean we can have co-fixed points?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 19:16):

seq is intended to be coinductive, and it has co-fixed points. It has all the same properties you would expect of such a coinductive def, if it existed

view this post on Zulip Mario Carneiro (Mar 27 2018 at 19:16):

except possibly the computation rules

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:19):

and what is the name of the fixed point function?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 19:20):

corec I think, depending on what you mean by co-fixed point

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:22):

I mean the sequence (1,2,1,2,...) being defined as X := 1,2,X

view this post on Zulip Mario Carneiro (Mar 27 2018 at 19:23):

We would need a better compiler to implement such a thing, but you can do it manually with a list storing the cycle

view this post on Zulip Kenny Lau (Mar 27 2018 at 19:24):

and then doing what?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:17):

Here's an implementation of cycle for stream: cycle 1 [2, 3] = [1, 2, 3, 1, 2, 3, ...]

def  cycle {α} (a : α) (l : list α) : stream α :=
stream.corec' (λ al, match al with
| (b, []) := (b, a, l)
| (b, c::l') := (b, c, l')
end) (a, l)

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:18):

no cycle [1,2,3]?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:22):

You could, but then what is cycle []?

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:23):

this way that's syntactically impossible to give as input

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:23):

if you did it in meta you wouldn't have to worry about this sort of thing, right?

view this post on Zulip Kevin Buzzard (Mar 27 2018 at 20:23):

and then you could just promise not to put [] in

view this post on Zulip Kenny Lau (Mar 27 2018 at 20:24):

I see

view this post on Zulip Mario Carneiro (Mar 27 2018 at 20:25):

You can promise not to put [] in in cycle as well: you could have an assumption l != [] which would be no fun to work with, or you could have A be inhabited so that it returns [default, default, ...] in that case, or you could return a seq so that this produces an empty seq


Last updated: May 16 2021 at 05:21 UTC