4 ms·
I've seen an impl somewhere where the (int => rat) bit from the Isabelle/HOL design was (stream rat). That's about the best I have at the moment.
by tel 11y ago
I've seen an impl somewhere where the (int => rat) bit from the Isabelle/HOL design was (stream rat). That's about the best I have at the moment.
- mafribe 11y agoBTW, in what sense is that coinductive? For what functor is it a final coalgebra?
- tel 11y agoStreams are coinductive, thus reals are the type of final coalgebras of (rat * -) which satisfy the Cauchy condition. So something like (Sigma (mu (rat * -)) isCauchy).
- mafribe 11y agoDon't you need to quotient after you've got Cauchy sequences? For example, (0,0,0,0,....) is a representative of the same real number (as Cauchy sequence) same as (1,0,0,0,0,0,....), but both are different as streams.
- tel 11y agoYeah, depends on how you're encoding it. Quotient types are to my knowledge still tricky to implement, but you can try to make a setoid and structure this type with some kind of equality. Of course, now we run directly into totality and semi-decidability.