Questions tagged [curry-howard]
The curry-howard tag has no usage guidance.
41 questions
1
vote
0
answers
39
views
What logical system does hindley-milner correspond to, according to the curry howard correspondence?
If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
- 36
2
votes
2
answers
62
views
What is "the ability of classical control operators to return multiple times from a single term"?
I am puzzled by a point in this paper by Phil Wadler.
Figure 6 shows a proof of the law of the excluded middle, $A ∨ ¬A$. The computational interpretation of this proof exploits the ability of ...
- 341
5
votes
4
answers
1k
views
Curry-Howard isomorphism and non-constructive logic
My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages.
...
- 241
4
votes
2
answers
130
views
Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic
Intuitionistic logic(s) are usually defined in a purely synthetic way, with their own deduction rules different from classical logic, but they also have semantic interpretations.
One of them, more ...
- 141
1
vote
1
answer
68
views
On the logical and categorical interpretation of lambda calculi and type systems
There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories.
Some variants of Barendregt's pure type systems have the property of strong ...
3
votes
2
answers
199
views
What are some examples of proofs that are also themselves "useful" programs?
With dependent types, types can be statements that are true or false and constructing a value with that type constitutes a proof of that statement. This proof/value construction is itself a program ...
- 219
2
votes
1
answer
113
views
Is the root function computationally equivalent to function application?
If a function type is representable by exponentiation, does it follow that function application is represented by the right inverse, roots? It would seem that roots consume a function's input to ...
- 21
2
votes
0
answers
93
views
How can we derive this representation of existential types?
I know that an existential type $ \exists t. t $ can be represented using universally quantified types as $ \forall r. (\forall t. t \rightarrow r) \rightarrow r $ and I have some basic intuition for ...
1
vote
0
answers
33
views
Analogue of disjunction and existence properties for a Turing-complete programming language?
Quoting from Wikipedia:
In mathematical logic, the disjunction and existence properties are
the "hallmarks" of constructive theories such as Heyting arithmetic
and constructive set theories ...
- 111
1
vote
0
answers
75
views
How do program types such as natural numbers figure into the Curry-Howard Isomorphism?
In Coq, the nat, the type of natural numbers, has type Set. By the Curry-Howard Isomorphism, all propositions of type ...
- 31
2
votes
1
answer
124
views
What are the differences between LCF's Theorem and Automath's Prop?
How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do ...
- 31
3
votes
2
answers
201
views
Curry–Howard correspondence and functional programming "reliability"
The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".
I recently ...
- 241
3
votes
1
answer
294
views
Curry-Howard, void, and type checking in Haskell
I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows.
Using the Curry-Howard isomorphism, construct an inhabitant of the type and ...
- 565
6
votes
0
answers
481
views
Understanding $\lambda \mu$-calculus in more programming way
I am learning $\lambda \mu$-calculus (self-study).
I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
- 295
5
votes
2
answers
667
views
Does the underlying computational calculus in type theories affect decidability?
I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers.
I understand that modern type theory is inspired by Curry-Howard ...
- 151
0
votes
0
answers
39
views
How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?
I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
- 175
2
votes
1
answer
197
views
Curry-howard isomorphism in object oriented programming languages
I want to get a better intuition for the curry howard isomorphism, and my intuition is mainly based on object oriented programming languages like JavaScript.
So as an example, I am going to formalize ...
- 277
6
votes
1
answer
466
views
Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence
I have to ask for forgiveness in advance if the whole question doesn't
make a lot of sense, but unfortunately, I have no better intuition as
of right now and this seems like the best starting point I ...
6
votes
1
answer
283
views
Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?
I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda ...
- 1,401
5
votes
2
answers
108
views
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
Recently I was reading again this propositions as types paper by Philip Wadler:
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
It gives an impression, ...
- 395
1
vote
1
answer
111
views
Is implication(function) more fundamental than lets say conjunction(product) in type theory?
According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they ...
- 35
4
votes
1
answer
278
views
How logic programming (especially ASP) is related to the reasoning in (first-order) logic?
How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
- 1,401
5
votes
1
answer
397
views
Can lambda-calculus be used for knowledge representation?
Natural language semantics (in computational linguistics) uses lambda terms for expressing the semantics of natural language sentences. There is vast literature about combinatorial categorial grammars ...
- 1,401
7
votes
1
answer
623
views
Curry Howard correspondence to Predicate Logic?
So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...
- 507
4
votes
0
answers
80
views
What is the role of abstract machines in the Curry-Howard isomorphism?
By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator...
According to Wikipedia page of the Curry-...
- 503
8
votes
1
answer
177
views
Can a type system serve as a proof assistant for foreign functions?
Given that:
A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO.
There are proof assistants that can be used to ...
- 295
3
votes
2
answers
870
views
forall a b, a -> b [duplicate]
I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$ (at least in a Hindley-Milner type system), but I can't wrap my head over it. ...
- 1,190
8
votes
2
answers
318
views
Why Church-encoded types aren't sufficient to express inductive proofs?
I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient ...
- 4,159
13
votes
1
answer
845
views
Is there an isomorphism between (subset of) category theory and relational algebra?
It comes from big data perspective. Basically, many frameworks (like Apache Spark) "compensate" lack of relational operations by providing Functor/Monad-like interfaces and there is a similar movement ...
- 243
1
vote
0
answers
54
views
Curry howard Isomorphism what the propositions A , B ranges over
In CH-I what the propositions A , B ranges over too ?
An update :
From Pfennings notes :
"A denotes proposition about the mathematical objects such as integer or a real number."
From :
Per ...
- 933
2
votes
0
answers
185
views
Curry howard isomorphism "proof as program"
I'm reading CH Isomorphism.
Let's divide into two stages:
Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B.
Proof corresponds to the program. What is the ...
- 933
3
votes
2
answers
151
views
relation between $\forall$ and implication in intuitionistic logic using curry-howard and propositions as types
I am currently trying to wrap my head around intuitionistic logic and its interpretation using the curry-howard isomorphism and propositions as types.
I came about this explained relation between $\...
- 591
14
votes
1
answer
947
views
Testing whether an arbitrary proof is circular?
I was thinking about proofs and ran into an interesting observation. So proofs are equivalent to programs via the Curry-Howard Isomorphism, and circular proofs correspond to infinite recursion. But we ...
- 141
5
votes
1
answer
359
views
Uses of the type Unit
The Unit type is a singleton type containing the constant unit. In functional languages with side effects, ...
- 173
7
votes
2
answers
752
views
In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?
(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm).
If I have a type signature ...
- 440
3
votes
3
answers
224
views
Isn't Domain of a variable nothing but a constraint?
In Constraint programming we have Variables and their Domains and then all the constraints, but if you at the concept of a domain of a variable it is nothing but another type of constraint, you are ...
- 628
1
vote
2
answers
1k
views
Curry Howard correspondence and Church-Turing thesis
Curry-Howard correspondence states the equivalence between logic/deduction and types/programs.
The Church-Turing thesis states the equivalence of some models of computation. Specifically, all ...
- 145
6
votes
2
answers
728
views
Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?
I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
- 347
18
votes
3
answers
2k
views
Does the Y combinator contradict the Curry-Howard correspondence?
The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
- 283
2
votes
2
answers
620
views
Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?
Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program.
We see ...
- 1,199
6
votes
1
answer
546
views
Non-termination of types in Martin-Löf's Type:Type?
In the pre-history of dependent type theory, Per Martin Löf
introduced a calculus that is in some sense the simplest dependent
type theory and the most general form of impredicative polymorphism.
It ...
- 8,358