20

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; Phil Wadler famously pointed out that the double-barrelled name "Curry-Howard" predicts other double-barrelled names like "Hindley-Milner" and "Girard-Reynolds"...


15

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 program go on forever is with recursion, and in terms of theory, usually we look at recursion as the $Y$ combinator, a program of type $\forall a \ldotp (a \to a) \...


13

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 cartesian closed category. I'm not going to spell out what a cartesian closed category is, though it isn't difficult, instead what the above statement says is you ...


10

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 to your theory. That being said, there are ways. In Coq for instance, there are various formalisations of the C standard (e.g. Robbert Krebbers' work). ...


9

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 propositions type systems to logical deduction systems If the type system admits a Y combinator, then that means that the corresponding logical deduction system is ...


8

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 of choice actually corresponds to some consistent logic. Different languages correspond to different logics, and many languages correspond to inconsistent ...


6

Short answer: yes. Long answer: For $\mathrm{Type}:\mathrm{Type}$, non-termination at the type level is trivial. You can take a constant $X:\mathrm{False}\rightarrow \mathrm{Type}$. Then if you take the inconsistent term $\bot : \mathrm{False}$ you have $$ X\ \bot : \mathrm{Type}$$ Which is non-terminating at the type level. You might complain that this has ...


6

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 formulas. There are also languages like Lolli, LolliMon, and Olli that work in fragments of linear logic (ordered linear logic in the last case). The concepts ...


6

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 logic a particular programming language represents. In particular, Haskell lacks dependent types. That means that it can't express statements with "forall x" or "...


5

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 your types are advanced enough to capture logic, then there's no algorithm which takes in a type and outputs a program of that type, if it exists. Just like ...


5

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 are more fundamental in Agda. That said, even there it's not completely clear cut. For example, Σ-types/pairs are introduced in Agda via inductive data type ...


5

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 could do $A=\top$ and $B = \bot$ and now true implies false! So, if it's not a true theorem, there's no proof of it, so the type is uninhabited. In a language ...


5

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 functions having that type in a typed lambda calculus, provided it is (weakly) normalizing. The intuition is that, as you mention, the associated proposition is ...


5

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 calculus of constructions.


5

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 approach) is HOL (= Higher-Order Logic). The most well-developed implementation of HOL is Isabelle/HOL (5). To the extent that you believe logic can represent ...


5

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 of type a, there exists a value of type [a]. The implementation of the function is the proof of the proposition. Here's a more detailed explanation: Basically, data constructors let us build ...


5

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 functions of arity 0 in strict languages that don't have zero-argument functions, like in OCaml: f (). Essentially this is just for deferring computations. (2) It also can be used to instantiate some parametrically polymorphic type when ...


4

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't Turing Complete. When you allow for non-halting programs, your logic becomes unsound. So the Curry-Howard Isomorphism doesn't really apply to Consider ...


4

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 computable. The Curry-Howard correspondence is a much stronger statement that certain types of intuitionistic logic are structurally identical to things kind ...


4

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-Howard correspondence, the types are much more precise and specified that what we'd normally deal with day-to-day. Moreover the Curry-Howard correspondence says ...


3

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 towards explaining what's wrong with my IsNat even though it seems very similar to Newsham.) Piponi page 17 on has: data Proposition = Proposition :-> Proposition | Symbol ...


3

"Theorems for free" are so-called because they follow from the type of the program, without looking at the the program code! "Contracts" are clearly not free theorems, because they depend on the code of the program, not merely the type. However, the connection you do want to make is between types and specifications. Specifications are in a way "more ...


3

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 [a] for any a so list types are always very easy to prove, in particularly they are trivially equivalent to any tautology that has already been proven. So ...


2

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 functions that do return a value, and one set that doesn't. You end up having to write somewhat duplicated higher order functions. One set of higher order functions ...


2

You are on your way to discovering the Curry-Howard correspondence.


2

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 have $s=\frac12$. But that upper bound is critical, because it defines the search space. RH is the statement that all of the zeroes lie on the critical line, ...


2

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 restricted domains is when you want to control very tightly the relations that are allowed to be used in constraints. For example, if you want to investigate the ...


1

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 natural numbers, trees, lists... are derivable. The core calculus doesn't have any datatype constructors packaged in. It starts at an extrinsic (curry style) ...


1

The difference between $s\to t$ and $\forall x : s. t$ is that in the second case, the return type of the function depends on the input. For example, in most languages, you can make a function that takes a natural number and returns an array of that size and it will have type $\operatorname{nat} \to \operatorname{nat} \operatorname{array}$. But if you want ...


1

Even though a domain may be considered just another type of constraint, there do exist good reasons to keep them separated, and it may be easier to think of them from a pure mathematical standpoint. Domains should in a sense be seen as the definition of the variable in terms of Type - e.g. Integer or Real etcetera. The domains can also be seen as the Master ...


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