Questions tagged [constructive-mathematics]
The constructive-mathematics tag has no usage guidance.
25
questions
13
votes
1
answer
895
views
Law of the Excluded Middle in complexity theory
A recent blog post by Lance Fortnow discusses non-constructive proofs, where "non-constructive" here means that the law of the excluded middle is used in a substantive way. That is, one ...
- 7,465
8
votes
3
answers
1k
views
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
Here is a Coq proof I've came up with:
...
- 212
5
votes
1
answer
210
views
Can you define recursive predicates in 2nd order intuitionistic logic?
This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.
Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) ...
- 13.7k
0
votes
1
answer
143
views
What is a known sequence for which being constant is not provable?
My question concerns the property of being constant for computable functions ${\mathbb N}\to \{0,1\}$, within any common framework $T$ strong enough to include Heyting arithmetic (and of course not ...
- 505
3
votes
1
answer
246
views
Is just one W-type enough for formalizing mathematics?
We work in intensional Martin-Löf type theory with $0$, $1$, $2$, $\Pi$, $\Sigma$, $W$ and a cumulative hierarchy of universes. Suppose our goal is to formalize constructive mathematics.
Now if we ...
user61651
5
votes
0
answers
162
views
Non-trivial existence proof in type theory
What are some examples of existence proofs in Coq/Agda etc., where the constructed natural number is useful from mathematical point of view, but it's non-obvious from the proof what it should be? I am ...
- 900
3
votes
0
answers
76
views
Monotonic and bounded sequences throughout computer science
When I refer to the Monotone Convergence Theorem below, I refer to the very simple claim that if a non-decreasing sequence has an upper bound then it converges. I don't refer to the claim from Measure ...
- 303
-4
votes
1
answer
133
views
4
votes
1
answer
152
views
Is the church-style affine calculus of constructions with unrestricted recursion consistent?
Suppose we take the church-style calculus of constructions, except with affine functions (variables must occur at most once) and mutual recursive definitions. For example:
...
- 3,117
3
votes
0
answers
223
views
Fast way of getting a matrix of sums
We are given an array of variables $A$, along with a matrix $M$. The elements of the matrix $M$ are composed of sums of the variables in $A$. We are allowed to pre-process $A$ in order to find a ...
- 2,100
12
votes
1
answer
342
views
What makes a language (and its type-system) capable of proving theorems about its own terms?
I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
- 3,117
1
vote
0
answers
85
views
Equality Theorems with Type Theoretic Proof
I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a ...
- 51
-2
votes
1
answer
113
views
Mathematical analogy to objects (as in object orientation)? [closed]
Data structures are similar to variables.
Algorithms to functions. Objects combine both data and algorithms. Is there a mathematical object / concept that combines variables and functions?
4
votes
2
answers
613
views
About the decidability of sets enumerated in non decreasing order
It is well known that a set of numbers enumerable in nondecreasing order is
decidable. However, the typical proof, by cases on the finiteness of the
enumerated set, is not constructive. In general, it ...
- 631
12
votes
2
answers
583
views
Implementing "Internal" Languages
One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
- 1,653
16
votes
3
answers
1k
views
Why do constructivists not seem to care too much about call/cc
So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
- 1,141
8
votes
3
answers
1k
views
What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?
I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
- 5,255
9
votes
1
answer
919
views
Equality of decidable proofs?
I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions.
Specifically, I want ...
- 93
4
votes
2
answers
280
views
Can programming help one understand constructive mathematics?
I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
- 121
0
votes
0
answers
104
views
Can I represent a computer program on a Hilbert Curve?
I overheard in discussion tonight:
You know - you can represent a computer program as points on a Hilbert Curve.
Is there a reference that explains this concept? I can't seem to Google for it.
- 2,581
2
votes
2
answers
649
views
Why is intuitionistic negation nonconstructive?
Can someone simply describe why intuitionistic negation is
not constructive and why intuitionistic proof is constructive?
in intuitionistic logic the notion of falsity has a 'subordinate' ...
- 21
6
votes
1
answer
755
views
Types which correspond to sets of cardinality of continuum
Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)?
On the first sight, they aren't, since elements of types are terms and we ...
- 1,762
7
votes
2
answers
336
views
SAT in some DTIME always via a constructive proof?
Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-...
- 81
26
votes
4
answers
2k
views
When does (or should) Theoretical CS care about intuitionistic proofs?
From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the ...
- 7,595
18
votes
3
answers
589
views
Constructively efficient algorithms without efficient correctness and efficiency proof
I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.
their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but
no proof using only ...
- 21.5k