Hacker News Reader

Comment by amelius | Hacker News Reader

How difficult would it be to write this in a formal system? How much space would it take?

Since real analysis is arguably the core of mathematics and of applications of mathematics, it has been formalised in many ways. See [1] for an overview of the state of the art.

[1] S. Boldo, C. Lelay, G. Melquiond, Formalization of Real Analysis: A Survey of Proof Assistants and Libraries., https://hal.inria.fr/hal-00806920v1/document

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.

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.)

The Coq standard library formalizes real analysis. Have a look at the "Reals" section:

https://coq.inria.fr/library/

You would need to get to the reals, which takes already a fair amount of time and includes a lot of machinery. Depending on how you constructed the reals, you might be able to reuse some concepts. So, it depends on where you start and which path you take.

Also, arguing by reference to the choice of appropriate values is incomplete argumentation and so it won't be accepted by a formal system. You'd have to fill these holes.

I'd suggest to start by evaluating the existing formalized constructions of the reals.

I think it is not too hard.

Reply on news.ycombinator.com