Questions tagged [constructive-mathematics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
23
votes
4answers
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 ...
17
votes
3answers
499 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 ...
15
votes
3answers
801 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 ...
12
votes
1answer
252 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 ...
9
votes
1answer
604 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 ...
8
votes
2answers
379 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 ...
7
votes
3answers
832 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 ...
7
votes
2answers
284 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-...
5
votes
1answer
490 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 ...
4
votes
2answers
244 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 ...
4
votes
1answer
99 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
votes
0answers
128 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
votes
1answer
128 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 ...
1
vote
2answers
349 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' ...
1
vote
0answers
77 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 ...
0
votes
0answers
92 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
votes
1answer
104 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?