Hacker News Reader

Comment by jojo3000 | Hacker News Reader

Even defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences:

http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html

This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically.

The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classical real analysis, based on topology and real-normed vector spaces.

View on HN

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.

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