15
votes
Accepted
Is there an isomorphism between (subset of) category theory and relational algebra?
Let me articulate the Curry-Howard-Lambek correspondence with a bit of jargon which I'll explain. Lambek showed that the simply typed lambda calculus with products was the internal language of a ...
- 12.1k
10
votes
Accepted
Can a type system serve as a proof assistant for foreign functions?
Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom ...
- 573
8
votes
Curry-Howard isomorphism and non-constructive logic
I think people sometimes disagree on what exactly Curry-Howard is. But, one way to look at it is an exact correspondence between the syntactic rules for logic and for type theory.
For the ...
- 2,927
7
votes
Accepted
Curry-Howard, void, and type checking in Haskell
I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also ...
- 2,275
7
votes
Accepted
Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence
Proofs in Haskell?
Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific ...
- 30.1k
6
votes
Accepted
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though.
Undecidability still holds for Curry-Howard: if ...
- 30.1k
6
votes
Accepted
How logic programming (especially ASP) is related to the reasoning in (first-order) logic?
Logic programming is proof search for some logic. Traditionally, this is the Horn clause fragment of first-order logic. Languages like lambdaProlog extend this to (intuitionistic) hereditary Harrop ...
- 12.1k
5
votes
Accepted
forall a b, a -> b
Think of this in terms of the Curry-Howard isomorphism. What would this type look like as a theorem?
For any propositions $A$ and $B$, $A \implies B$.
Clearly this is not true, if it were, then we ...
- 30.1k
5
votes
forall a b, a -> b
I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$, but I can't wrap my head over it.
No, that type is not inhabited. There are no ...
- 14.7k
5
votes
Accepted
Why Church-encoded types aren't sufficient to express inductive proofs?
How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction
principle and the axiom of
choice in the pure ...
- 8,358
5
votes
Accepted
Can lambda-calculus be used for knowledge representation?
The λ-calculus was invented to be a logic and foundation of mathematics (1-4). The most well-known logic to use λ-calculus for formulae (as opposed to proofs in the Curry-Howard ...
- 8,358
5
votes
Accepted
Is implication(function) more fundamental than lets say conjunction(product) in type theory?
For Agda, I think, as stated in the other question, that the fact that function types (or rather Π-types) are built-in while pairs (or even Σ-types) aren't so much is a reasonable argument that they ...
- 12.1k
4
votes
Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?
You are on your way to discovering the Curry-Howard correspondence.
- 31.2k
4
votes
Does the underlying computational calculus in type theories affect decidability?
I don't think that the term "modern" helps distinguish anything. One way to explain is to draw a distinction between "behavioral", or "semantic", type theories and "formal", or "syntactic", type ...
- 141
4
votes
Curry–Howard correspondence and functional programming "reliability"
The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function.
...
- 31.2k
3
votes
Accepted
What are some examples of proofs that are also themselves "useful" programs?
Many constructive proofs could be useful. For example, to prove that every set of points in the plane (in general position) have a Delaunay triangulation, you would give the algorithm for producing ...
- 156
3
votes
Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic
Both Kripke semantics and propositions-as-types interpretation are sound and complete for the intuitionistic propositional calculus. In this sense they are equivalent.
However, there are formulas in ...
- 31.2k
3
votes
Curry-Howard isomorphism and non-constructive logic
The Curry-Howard correspondence is not crucial for functioning of a proof assistant. Unforunately, the term "Curry-Howard correspondence" seems to be misused nowadays for all sorts of things....
- 31.2k
3
votes
Curry-Howard isomorphism and non-constructive logic
While proof assistants typically use constructive mathematics, the Curry-Howard-Correspondence does not necessarily require constructivism.
The important aspect of the correspondence is that the ...
- 131
3
votes
Curry Howard correspondence to Predicate Logic?
To explain why I'm uncomfortable with Newsham's and (especially) Piponi's data wrappers ... (This is going to be more question than answer, but perhaps it'll work ...
- 507
3
votes
Does the underlying computational calculus in type theories affect decidability?
You are probably looking for computational type theory and you should probably look into realizability theory as well, which explains how to interpret type theory (and higher-order logic) on top of ...
- 31.2k
2
votes
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
The programs that you describe are very good at searching for zeroes in an interval; they can find all of the zeroes of the form $s+it$ between $t=0$ and $t=10^9$, say, and show that all these zeroes ...
- 2,529
2
votes
What is "the ability of classical control operators to return multiple times from a single term"?
The control operators in question allow you to capture continuations such that calling the continuation is in some sense equivalent to "returning from" the expression. so, for instance, in (...
- 2,927
2
votes
Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic
For propositional logic, you're probably right. As far as quantifier logic goes: the Curry-Howard correspondence never included quantifiers and there isn't really any consensus or standard treatment ...
- 379
2
votes
On the logical and categorical interpretation of lambda calculi and type systems
(My answer is only about how non-termination relates to inconsistency.)
The general idea of the Curry-Howard correspondence is that a term having a type, corresponds to a proof for a theorem. A term ...
1
vote
What are the differences between LCF's Theorem and Automath's Prop?
The difference is in what kind of type theorem/Prop is.
In Isabelle, theorem is a type in ...
1
vote
Curry–Howard correspondence and functional programming "reliability"
The type system in FP languages helps you avoid a certain number of errors. The more you use various features of the type system, the more errors you can exclude.
For example, if you need the list of ...
- 291
1
vote
Curry-howard isomorphism in object oriented programming languages
If you only consider terminating functions, then your axiomatisation works :-) Indeed, terminating functions have a resonable notion of equality:
If their return type has decidable equality then the ...
- 894
1
vote
Why Church-encoded types aren't sufficient to express inductive proofs?
There is a result recently published within Annals of Pure and Applied Logic in which church encoded data are realizers of their own induction principle. In this system, the induction principle for ...
- 11
Only top scored, non community-wiki answers of a minimum length are eligible