Hacker News Reader

Comment by mafribe | Hacker News Reader

I wonder if the coinductive approach calculus by Pavlovic et al [1, 2] has been considered as a basis for formalisation.

I secretly hope that I will one day get to teach calculus to computer scientists. In that case I would introduce reals as a coinductive data type, and the usual operations (such as differentiation, integration, solving differential equations) as stream operations. That should appeal to programmers, athough it would be weird for conventional mathematicians.

[1] D. Pavlovic, M. Hölzl Escardo, Calculus in coinductive form.

[2] D. Pavlovic, V. Pratt, The continuum as a final coalgebra.

View on HN

I haven't read the paper, but if you define the reals as constructive Cauchy sequences you'd be forced into a coinnductive definition. Is that equivalent?

I'm not familiar with constructive Cauchy sequences. The usual way of using Cauchy sequences is to quotient them by the ideal of Cauchy sequences that converge to 0.

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.

BTW, in what sense is that coinductive? For what functor is it a final coalgebra?

Streams are coinductive, thus reals are the type of final coalgebras of (rat * -) which satisfy the Cauchy condition. So something like (Sigma (mu (rat * -)) isCauchy).

Don'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.

Yeah, 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.

In constructivism, once you have a Cauchy sequence of rationals, that represents a real. However given two such Cauchy sequences, you cannot always prove whether one is less than, equal to, or greater than the other.

This has some interesting consequences. For example only continuous functions can be functions in constructivism. (If you try to construct a function that is discontinuous at a point, there are Cauchy sequences you can give it that you cannot assign to a Cauchy sequence coming out. So it is not a well-defined function.)

Reply on news.ycombinator.com