Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [curry-howard]

The tag has no usage guidance.

0
votes
0answers
19 views

What is an intuitive way to understand the definition of Curry and Uncurry in Categorical Language?

I was studying the definition of currying and uncurrying using Category Theory from these slides. The answer and the proof on slide 19 makes 100% sense to me however, the definitions seem to come out ...
1
vote
1answer
36 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 ...
5
votes
1answer
222 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 ...
5
votes
1answer
139 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 ...
3
votes
2answers
78 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, ...
1
vote
1answer
44 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 ...
4
votes
1answer
90 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 ...
5
votes
1answer
253 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 ...
7
votes
1answer
354 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 ...
4
votes
0answers
59 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-...
9
votes
1answer
100 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 ...
3
votes
2answers
632 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. ...
6
votes
2answers
120 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 ...
11
votes
1answer
418 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 ...
1
vote
0answers
50 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 ...
1
vote
0answers
121 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 ...
1
vote
1answer
79 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 $\...
12
votes
1answer
892 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 ...
5
votes
2answers
206 views

Uses of the type Unit

The Unit type is a singleton type containing the constant unit. In functional languages with side effects, ...
6
votes
2answers
575 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 ...
3
votes
3answers
135 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 ...
1
vote
2answers
430 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 ...
5
votes
2answers
440 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 ...
15
votes
2answers
744 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 ...
2
votes
2answers
497 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 ...
5
votes
1answer
330 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 ...