Constructive mathematics and computer programming (1979) [pdf]
1–10 of 23 posts
Re: Constructive mathematics and computer programming (1979) [pdf]
#2Per Martin-Löf writes so beautifully.
Here’s more: https://github.com/michaelt/martin-lof
Here’s another one - this one is wonderful: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo...
As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory
Intuitionism in math is beautiful imo: https://en.wikipedia.org/wiki/Intuitionism
Re: Constructive mathematics and computer programming (1979) [pdf]
#3Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today.
I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper. https://lamport.azurewebsites.net/tla/tla.html
Re: Constructive mathematics and computer programming (1979) [pdf]
#4Thanks, I'll copy this to my tablet so I can carry it around with me.
Looking forward to being impressed (hopefully) that it is still relevant today.
Re: Constructive mathematics and computer programming (1979) [pdf]
#5As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research?
I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
Re: Constructive mathematics and computer programming (1979) [pdf]
#6As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that thi…
I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
Re: Constructive mathematics and computer programming (1979) [pdf]
#7As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that thi…
One exciting new development is "Cubical Type Theory: a constructive interpretation of the univalence axiom" [0], a constructive version of homotopy type theory.
The "axiom of choice" in this context is not really an axiom, just a provable theorem whose proof in this setting is given by Martin-Löf. The reason, I believe, is that constructive mathematics has a different meaning for the exists (∃) quantifier. In a constructive context, existence is "stronger" since you have to specify a witness of existence; this makes the hypothesis of the "axiom" of choice stronger, allowing for a proof.
Here's a stab at a very informal version of this. Suppose you have a set composed of "slices". The "axiom" of choice says that "IF for every slice (x in A) there exists a good element of that slice (y in B_x, and 'good' is defined by satisfying property C), THEN there exists a function which takes a slice and returns a good object of that slice." But the very definition of the (constructive) word "exists" in the hypothesis means you already have to specify, as input, a way of finding one good object of each slice. With this, finding a function that provides a good object of each slice is a tautology.
Re: Constructive mathematics and computer programming (1979) [pdf]
#8As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that thi…
I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way.
> The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory.
I'm getting confused because Martin-Lof writes at the end of this paper:
> I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice...
Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.
Re: Constructive mathematics and computer programming (1979) [pdf]
#9As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research? I'm also curious if someone can weigh in on the fact that thi…
One exciting new development is "Cubical Type Theory: a constructive interpretation of the univalence axiom" [0], a constructive version of homotopy type theory. The "axiom of choice" in this context is not really an axiom, just a provable theorem whose proof in this setting is given by Martin-Löf. The reason, I believe, is that constructive mathematics has a different meaning for the exists (∃) quantifier. In a cons…
Thank you, this helps my understanding.
Re: Constructive mathematics and computer programming (1979) [pdf]
#10Earlier quoted context omitted.
I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way. > The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand a…
I'm confused then because the paper linked in the OP states:
> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]