Email Gateway (Aug 22 2022 at 19:14): Email Gateway (Aug 22 2022 at 19:14):From: Dominique Unruh <unruh@ut.ee>
This is a thing I've always wondered about:
Is there a formal reason why dependent type theory and constructive
logic tend to come together (e.g., difficulties in soundly integrating
the LEM or something),
or is that more of a community thing, i.e., the people who like type
theory just happen to also like constructive math?
Best wishes,
Dominque.
Email Gateway (Aug 22 2022 at 19:14):From: Freek Wiedijk <freek@cs.ru.nl>
Hi Dominique,
There certainly are also type theories for classical math
("lambda-bar mu mu-tilde" comes to mind :-)), but they are
more complicated and less trivially computational than the
normal type theories, which correspond to constructive math.
So it's not just a community thing, I think.
Basically, throwing an exception corresponds to the
ex-falso rule, and catching it corresponds to LEM, or
rather to elim-style rule "(~A ==> B) ==> (A ==> B) ==> B",
which amounts to the same thing. In other words,
constructivists only get half of the exception mechanism:
they can throw, but can't catch.
However you can take an exception and run with it, so to
implement this in an implementation, you really need to
save the full state of the system (including the stack and
heap and everything) in an exception. For Lisp this is the
"call-with-current-continuation" function.
So constructive math is functional programming without
exceptions. And using an exception monad instead of built-in
exceptions corresponds to the double negation translation :-)
Freek
Email Gateway (Aug 22 2022 at 19:15):From: Dominique Unruh <unruh@ut.ee>
Hi,
I have to admit that I didn't really get the connection between
exceptions and LEM.
But it seems to me what you explained is why it is problematic to give
computational meaning to a theory with LEM, right? That much I get.
But I don't see why dependent type theories have to necessarily come
with a computational meaning. (It could again be a community thing:
people doing types like computation.)
Basically, as I see it, the idea in classical math is that we do not
care about a computational meaning of our formulas. (While
constructivism does.)
So, my question would be: is there an inherent reason why dependent type
theory is more difficult if we want LEM and do not care about computability?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:15):From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Am Montag, den 25.02.2019, 18:13 +0200 schrieb Dominique Unruh:
Hi,
I have to admit that I didn't really get the connection between
exceptions and LEM.But it seems to me what you explained is why it is problematic to give
computational meaning to a theory with LEM, right? That much I get.
Yes, LEM breaks computation, as it is a axiom without a computational
rule.
And this is a distinction which is usually done in dependent type
theory, but not in HOL: axioms and computational rules. In HOL there
are no computation rules besides alpha and eta equivalence and beta
reduction. While in DTT a lot of people prefer not to have any
constants which do not have a computation rule associated with them,
but often do not have a problem with introducing complex type formers
as long as one can compute with it.
HOL:
oh is is a small logic, only AC+LEM+funext+propext+typedef+...
and then we derive (co)datatypes
DDT:
oh it is a small logic, no "axioms" but a powerful datatype formers
so we can do a lot of (constructive) mathematics.
But in many cases both approaches can be merged, in Coq you can use the
Axiom of Choice. And in Lean we use it by default. On the other hand,
if you want to go to HoTT you can't use Axiom of Choice on arbitrary
types (but still on the HOL subset of HoTT)
But I don't see why dependent type theories have to necessarily come
with a computational meaning. (It could again be a community thing:
people doing types like computation.)
Yes, this is usually the case. The advantage of using a limited logic
is that one gets additional properties for free. When you write down a
function in HoTT (without classical axioms) you get a continuous
function, where continuity is for free.
Basically, as I see it, the idea in classical math is that we do not
care about a computational meaning of our formulas. (While
constructivism does.)
Yes.
So, my question would be: is there an inherent reason why dependent type
theory is more difficult if we want LEM and do not care about computability?
I would not say that dependent type theory is more difficult with LEM.
It is as difficult as HOL.
What you miss if you don't enjoy computability of your constants is
powerful unification/definitional equality! For example, a lot of proof
steps where the simplifier is used in Isabelle are just application of
one rule in Lean. Mind: definitional equality breaks abstraction (often
the definition should not be part of an module interface), but for many
basic constants this is a huge bon. ssreflect and mathcomp uses it a
lot.
So, yes it gets more difficult: one needs a powerful rewrite engine
like in Isabelle.
Best wishes,
Dominique.
On 2/25/19 1:42 PM, Freek Wiedijk wrote:
Hi Dominique,
Is there a formal reason why dependent type theory and
constructive logic tend to come together (e.g., difficulties
in soundly integrating the LEM or something), or is that
more of a community thing, i.e., the people who like type
theory just happen to also like constructive math?
There certainly are also type theories for classical math
("lambda-bar mu mu-tilde" comes to mind :-)), but they are
more complicated and less trivially computational than the
normal type theories, which correspond to constructive math.
So it's not just a community thing, I think.Basically, throwing an exception corresponds to the
ex-falso rule, and catching it corresponds to LEM, or
rather to elim-style rule "(~A ==> B) ==> (A ==> B) ==> B",
which amounts to the same thing. In other words,
constructivists only get half of the exception mechanism:
they can throw, but can't catch.However you can take an exception and run with it, so to
implement this in an implementation, you really need to
save the full state of the system (including the stack and
heap and everything) in an exception. For Lisp this is the
"call-with-current-continuation" function.So constructive math is functional programming without
exceptions. And using an exception monad instead of built-in
exceptions corresponds to the double negation translation :-)Freek
Email Gateway (Aug 22 2022 at 19:15):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Dominique wrote:
Is there a formal reason why dependent type theory and constructive
logic tend to come together (e.g., difficulties in soundly integrating
the LEM or something),
or is that more of a community thing, i.e., the people who like type
theory just happen to also like constructive math?
I quote from nlab: https://ncatlab.org/nlab/show/Boolean+topos
The internal logic of a Boolean topos with natural numbers object can serve
as foundations for "ordinary" mathematics, except for that which relies on
the axiom of choice. If you add the axiom of choice, then you get (an
internal version of) ETCS [Elementary Theory of the Category of Sets];
conversely, if you use an arbitrary topos, then you get constructive
mathematics.
Dependent type theory corresponds to the internal logic of an arbitrary
topos. The particular case of a dependent type theory, in which the LEM was
accepted, corresponds to the internal logic of a Boolean topos. Reference
about the relationship between topos theory and dependent type theory:
http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf
A concrete example.
On the one hand, the topos to formalize the Birkhoff -von Neumann quantum
logic is a Boolean topos, because it is just classical mathematics (it is
natural to formalize it in Isabelle/HOL). On the other hand, the topos used
to formalize the "intuitionistic" version of Birkhoff -von Neumann quantum
logic (in which LEM does not hold, but the distributive property holds) is
the Bohr topos (this is not a Boolean topos). Some references:
nlab: https://ncatlab.org/nlab/show/Bohr+topos
video-lecture: https://youtu.be/bNPNiEHXYPM
In which proof assistant a formalization of the theory of Bohr topos is
more natural? I doubt that the dependent type theory of Coq (CIC)
corresponds to the internal logic of a Bohr topos. I guess that such a
proof assistant does not exist yet.
Kind Regards,
José M.
Last updated: May 06 2024 at 12:29 UTC