Higher-order logic and equality; multiple ways to use lambda calculus for logic
blog.burakemir.ch
blog.burakemir.ch
I'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA
��Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Not entirely. There are type errors that are caught at compilation time.
A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error.
And types are checked at run time as well.
I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include:
* If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages.
* Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense.
* Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities.
* Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
* The English language is far more powerful than any programming language.
* All logic is really just intuitionistic logic.
* All logic is really just linear logic.
* Syntactic formalism must be wrong, because abstracta only exist in my mind.
To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely.
[0] https://ncatlab.org/nlab/show/relation+between+type+theory+a...
Obviously it's all really just tensorial logic :^)
> * All logic is really just linear logic.
and
> * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.
> All logic is really just linear logic.
Who has said these?
Abstract:
> A uniform representation, as binary trees with empty leaves, is given to expressions built with Rosser's X-combinator, natural numbers, lambda terms and simple types. Type inference, normalization of combinator expressions and lambda terms in de Bruijn notation, ranking/unranking algorithms and tree-based natural numbers are described as a literate Prolog program.
> With sound unification and compact expression of combinatorial generation algorithms, logic programming is shown to conveniently host a declarative playground where interesting properties and behaviors emerge from the interaction of heterogenous but deeply connected computational objects.
I don't believe this is very common—it's _an_ intuitionist logic, but "intuitionistic logic" by itself pretty much always includes ex falso—but actually it's rather strange that this is the case; it's not immediately clear that ex falso is constructive at all!
Minimal logic is both 'intuitionistic' (since LEM does not hold) and paraconsistent (since ex falso does not hold). I actually think there's a fairly solid case to say that only paraconsistent logics can be thought of as truly constructive; certainly if we start from BHK, it's not at all obvious that ex falso is a sound principle, and Kolmogorov himself had great issues accepting this. When he finally managed to convince himself of this in 1932 [1], it seems more that he was trying to finish off the logical framework by sidestepping the issue.
Kapsner [2] argues that the constructivist can only accept ex falso if she is willing to accept so called "empty promise constructions" as being constructive (see the source for more details on what this means, but it seems to broadly line up with Kolmogorov's justification); I personally don't think that they are compatible with the way BHK is usually presented at all.
Brouwer isn't around to tell us exactly what _he_ means by constructivism, so ultimately this is all philosophical, but I think this it's an interesting area that people don't really think aboutl I think a lot of people are exposed to intuitionistic logic via Martin-Lof type theories but don't actually consider how the logic fits into the wider notion of constructivism.
[1] : https://plato.stanford.edu/entries/intuitionistic-logic-deve...
This is an exposition of Martin-Lof's dependent type theory: http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs17.pdf Section 5 is about Homotopy Type Theory (HoTT), a newer type theory that is still being developed.
Chapter 1 of the HoTT book introduces Martin-Lof's dependent type theory, then the rest of the book covers HoTT-specific topics: https://homotopytypetheory.org/book/
That's an entire book that is merely a guide on which other books to read and what to focus on in one's journey of formal logic.
I have started with the most intro book it recommends "How to Prove It : A Structured Approach by Daniel J. Velleman". It seems to be quite similar to whatever text book I used in the class that focused on logic in college. I intend to skip around a bit though as my real goal here is to be able to understand all of this advanced type theory that I keep seeing in the FP/Haskell/Idris world.
I find the discussion in of logic in https://sites.math.northwestern.edu/~richter/HolInformalMath... more concrete and more accessible.
Ref: https://cs.stackexchange.com/questions/122066/does-the-under...
https://en.wikipedia.org/wiki/Natural_deduction
The short version is that
A B
-------
C
A B
-------
C D
---------
E
The rules
A B
-----
C
A B
----- (→c)
C
Additionally, I would be careful about correcting others that something is "technically" called something else as programming language researchers often use many names for the same concept.
My point had nothing to do with programming language research (in fact, my academic background is logic/metalogic). And by the way, this is not a rule:
A B
----- (→c)
C
[1] https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...
A → B A
-----------
B
Things can get complicated, but they aren't always complicated so naming rules isn't strictly necessary.