Questions tagged [constructive-mathematics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
13 votes
1 answer

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 ...
Timothy Chow's user avatar
  • 7,465
8 votes
3 answers

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: ...
Zazaeil's user avatar
  • 212
5 votes
1 answer

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) ...
cody's user avatar
  • 13.7k
0 votes
1 answer

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 ...
Nikolaj-K's user avatar
  • 505
3 votes
1 answer

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 ...
user avatar
5 votes
0 answers

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 ...
Ilk's user avatar
  • 900
3 votes
0 answers

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 ...
wlad's user avatar
  • 303
-4 votes
1 answer

conversion to DAG

Can we reverse directions instead?
HHH's user avatar
  • 7
4 votes
1 answer

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: ...
MaiaVictor's user avatar
  • 3,117
3 votes
0 answers

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 ...
Matt Groff's user avatar
  • 2,100
12 votes
1 answer

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 ...
MaiaVictor's user avatar
  • 3,117
1 vote
0 answers

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 ...
Krpcannon's user avatar
-2 votes
1 answer

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?
A.L. Verminburger's user avatar
4 votes
2 answers

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 ...
Andrea Asperti's user avatar
12 votes
2 answers

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 ...
Max New's user avatar
  • 1,653
16 votes
3 answers

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 ...
Jake's user avatar
  • 1,141
8 votes
3 answers

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 ...
PhD's user avatar
  • 5,255
9 votes
1 answer

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 ...
Adam Barak's user avatar
4 votes
2 answers

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 ...
Ali's user avatar
  • 121
0 votes
0 answers

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.
hawkeye's user avatar
  • 2,581
2 votes
2 answers

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' ...
Shahab's user avatar
  • 21
6 votes
1 answer

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 ...
Konstantin Solomatov's user avatar
7 votes
2 answers

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-...
user20264's user avatar
26 votes
4 answers

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 ...
usul's user avatar
  • 7,595
18 votes
3 answers

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 ...
Kaveh's user avatar
  • 21.5k