21 votes
Accepted

Does the Y combinator contradict the Curry-Howard correspondence?

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus. There are, of course, other Curry-Howard-like isomorphisms; ...
user avatar
  • 18.9k
15 votes

Testing whether an arbitrary proof is circular?

The vast majority of proof systems don't allow for infinite, circular proofs, but they do so by making their langauges non-Turing complete. In a normal functional language, the only way to make a ...
user avatar
  • 29.1k
14 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 ...
user avatar
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 ...
user avatar
  • 563
9 votes

Does the Y combinator contradict the Curry-Howard correspondence?

The Curry-Howard relates type systems to logical deduction systems. Among other things, it maps: programs to proofs program evaluation to transformations on proofs inhabited types to true ...
user avatar
9 votes
Accepted

Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?

Proving the correctness of a program in a form of a proof that's nothing but the program itself This is not quite how the Curry-Howard-Correspondence works. First one has to show that the language ...
user avatar
  • 404
6 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 ...
user avatar
  • 29.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 ...
user avatar
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 ...
user avatar
  • 29.1k
6 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 ...
user avatar
  • 1,399
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 ...
user avatar
  • 29.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 ...
user avatar
  • 14.2k
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
5 votes
Accepted

Uses of the type Unit

Some other usages of the type Unit (I'm sure the list is not exhaustive): (1) The value of type Unit is used to simulate ...
user avatar
  • 3,419
5 votes

Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?

In some sense it doesn't matter what the function does, as long as it takes the correct types and produces something of the correct type. The trick is that when you start talking about the Curry-...
user avatar
5 votes
Accepted

In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

One way to interpret types as logic is as the existence conditions for values of the return type. So f :: a -> [a] us the theorem that, if there exists a value ...
user avatar
  • 29.1k
4 votes

Curry Howard correspondence and Church-Turing thesis

TLDR: A sound logic corresponds to a non-Turing-complete lambda calculus, so the Church-Turing thesis doesn't apply. It's important to remember that most Dependently Typed programming languages aren'...
user avatar
  • 29.1k
4 votes
Accepted

Curry Howard correspondence and Church-Turing thesis

I'm not sure where you see the dissonance. The Church-Turing thesis is a hypothesis stating that Turing Machines (equiv. Lambda Calculus or Recursive Functions) can do anything that we'd think of as ...
user avatar
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 ...
user avatar
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. ...
user avatar
  • 28.2k
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 ...
user avatar
  • 477
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 ...
user avatar
  • 28.2k
3 votes

In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

List types are a bit strange as proposition. They don't really correspond to anything directly familiar but it is easy to see what they are equivalent to. Because nil exists you can always prove ...
user avatar
  • 3,728
2 votes

Uses of the type Unit

I can think of a couple: If a language makes a distinction between functions that return a value, and those that don't, it becomes difficult to stitch functions together. You have one set of ...
user avatar
  • 21
2 votes
Accepted

Isn't Domain of a variable nothing but a constraint?

As you observe, restricting the domain of a variable has exactly the same effect as applying a unary constraint to it. One situation where you might prefer to use unary constraints rather than ...
user avatar
2 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.
user avatar
  • 28.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 ...
user avatar
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 ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible