The Coq mailing list

[Neelakantan Krishnaswami <n.krishnaswami AT cs.bham.ac.uk>]

Hello,

My understanding is that if you want to work with constructive reals,
and you also want to print out decimal expansions[*], one solution is
to

(a) extend type theory with a monadic type constructor M(-) for
    nondeterminism, and
(b) treat printing as a function Real -> Nat -> M(String),
    where the Nat is the number of digits to print).

The idea is that printing is a constructively realizable operation:
ie, for every real r and natural number n, there exists a decimal
expansion of its first n digits. However, this realizer is (in Bishop's
terminology) an *operation* rather than a *function*. This means
different representations of the same real may print different decimal
expansions. So the realizer doesn't respect equality on the reals, and
hence cannot be a function.

So, constructively, you can view printing as a multivalued function,
or equivalently as a function into some kind of powerset/powerdomain.

Given how Nurpl is structured as a theory of realizers, there's probably 
something very cunning you can do with this idea.


Best,
Neel


PS. Andrej Bauer has told me that this is essentially what people
working in Weihrauch's Type Two Effectivity do, but you would need to
ask him for details.

[*] There are technical issues to do with needing negative digits to
implement all the operations (such as addition and multiplications)
using Cauchy sequences, but the solutions are known and so we can
neglect them in this email.

On 25/09/15 22:20, Abhishek Anand wrote:
> I totally agree with Arnaud's point about reals.
> I just want to emphasize the importance of the ability to get rational
> approximations of (constructive) reals.
>
> I have been using constructive reals for writing certified Coq programs
> for robots [1] and actually running them on actual robots.
> Unlike floating points, at most places I don't have to worry about
> inexactness. For example, field laws hold exactly, and sin^2 x + cos^2 x
> is /exactly/ equal to 1.
> However, in the end when all the computation is done, and it is time to
> send some commands to hardware, such as timers, or motor drivers, I
> cannot send them constructive reals.
> Instead, I /have to approximate them to a sufficiently simple rational/,
> e.g. a timer accepts a millisecond value, and iRobot Create
> <http://www.irobot.com/About-iRobot/STEM/Create-2.aspx> accepts an 8-bit
> value representing the requested speed for its motors.
>
> [1] Abhishek Anand and Ross Knepper. “ROSCoq: Robots powered by
> constructive reals”. In: ITP. Aug.
> 2015. https://github.com/aa755/ROSCoq.
>
>
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
>
> On Fri, Sep 25, 2015 at 2:19 PM, Arnaud Spiwack
> <aspiwack AT lix.polytechnique.fr
>  
> <mailto:aspiwack AT lix.polytechnique.fr>>
> wrote:
>
>     There is a lot to say about the type theory of setoids. I'll attempt
>     to share some of my thought on it.
>
>     As Neel said already, OTT is such a theory. It does not have a very
>     good story for universes, though, univalence can be seen as a way to
>     address this particular issue.
>
>     Another difficulty is how to treat quotient types. I don't remember
>     very well how they are handled in OTT, though I remember they were
>     pretty convincing. Though they can be seen as a generalisation of
>     quotients, higher inductive types are really a rather different
>     angle on this question (though I may be wrong).
>
>     Setoids serve two purposes: adding some extensionality, and adding
>     quotients to the theory of Coq. Both are rather tricky balancing
>     games when you want to preserve the computational behaviour of Coq
>     (if you don't care about computation, you can just posit
>     extensionality and axiomatise quotient types, there are probably
>     pitfalls in the case of quotient types, though, has someone looked
>     into it?).
>
>     There are two things which I'd consider limits of this approach,
>     however. First you would probably need a setoid rewriting thing in
>     the tactics nonetheless: it handles more than setoids (like
>     ordering) and it is useful for simplification by rewriting (just
>     using `repeat rewrite` is terrible for your perfs). The second is
>     that there are things which are doubtful when expressed as quotient
>     types, like the real numbers: real numbers can be seen as a quotient
>     of, say, function from the natural numbers to the rational
>     (returning an approximation up to 2⁻ⁿ). But if you do so, there is
>     no way, in the theory of setoids, to extract an approximation of a
>     real, as it's not a function which respects the quotient equality.
>     So there are extra complications there (maybe a type a functions
>     which are explicitly not equality preserving, but it's not really
>     easy to use).
>
>     Of course, there is much unnecessary tedium associated with proofs
>     with setoids, and here's to hoping a solution is found some day. But
>     as you see: it's not easy.
>
>
>     On 25 September 2015 at 18:52, Gabriel Scherer
>     
> <gabriel.scherer AT gmail.com
>  
> <mailto:gabriel.scherer AT gmail.com>>
>  wrote:
>
>         You may be interested in Marc Lasson's paramcoq plugin, which
>         generates parametricity witnesses from Coq terms. (So it's not
>         trying
>         to internalize the fact that terms respect
>         equality/parametricity, but
>         rather make the meta-theorem available in practice as a
>         meta-programming tool.)
>
>         https://github.com/mlasson/paramcoq
>
>         On Fri, Sep 25, 2015 at 4:37 PM, Neelakantan Krishnaswami
>         
> <n.krishnaswami AT cs.bham.ac.uk
>         
> <mailto:n.krishnaswami AT cs.bham.ac.uk>>
>  wrote:
>          > On 25/09/15 13:35, Ilmārs Cīrulis wrote:
>          >>
>          >> I often have to use Equivalence and Proper (while tinkering
>         around),
>          >> therefore a question appeared:
>          >>
>          >> What about Coq (or any other proof assistant / type theory)
>         where
>          >> setoids and morphisms are first class citizens (built in,
>         replacing
>          >> standard Type and function that becomes something like lower
>         level of
>          >> language). In such case there would be no need of special
>         libraries for
>          >> Equivalence, Setoid and related libraries for, e.g., lists
>         or other data
>          >> structures that respects equivalence.
>          >>
>          >> What are cons of such idea?
>          >
>          >
>          > This is essentially the idea behind Observational Type
>         Theory; you
>          > should look at:
>          >
>          > * Extensional Equality in Intensional Type Theory. T. Altenkirch
>          >   LICS 1999
>          > * Observational equality, now! T. Altenkirch, C. McBride, W.
>         Swierstra,
>          >   PLPV 2007
>          >
>          > The core idea (every type is a setoid and every definable
>         term is a
>          > equality-respecting morphism) is very simple, but making all
>         the syntax
>          > line up to make it work is tricky and intricate.
>          >
>          > Best,
>          > Neel
>          >