undefined | Better HN

0 pointsmafribe9y ago0 comments

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

0 comments

5 comments · 1 top-level

dvt9y ago· 4 in thread

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination:

Let α → H be a functional type where α is a Person type, and H is a boolean type.

   Γ ⊢ α → H     Γ ⊢ α
  --------------------- (→e)
            Γ ⊢ H

What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true:

  A → B
  A
  ∴ B

(I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.)

[1] http://dvt.name/logic/horse2.pdf

chriswarbo9y ago

Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)

dvt9y ago

> Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.

Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).

mafribeOP9y ago

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

dvt9y ago

There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much.

All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have.

[1] http://plato.stanford.edu/entries/logic-paraconsistent/

1 more reply

j / k navigate · click thread line to collapse

0 comments

5 comments · 1 top-level

dvt9y ago· 4 in thread

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination:

Let α → H be a functional type where α is a Person type, and H is a boolean type.

   Γ ⊢ α → H     Γ ⊢ α
  --------------------- (→e)
            Γ ⊢ H

  A → B
  A
  ∴ B

(I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.)

[1] http://dvt.name/logic/horse2.pdf

chriswarbo9y ago

Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

dvt9y ago

> Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.

Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).

mafribeOP9y ago

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

dvt9y ago

There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much.

All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have.

[1] http://plato.stanford.edu/entries/logic-paraconsistent/

1 more reply

j / k navigate · click thread line to collapse