Derivation rules kind of look like fractions, don't they? Let's try applying our usual calculation rules for fractions and see what we get.
×
=
Hmm. If we interpret A B to mean A∧B, that makes sense. By multiplying two rules, we get another valid rule, for if we know that A→B and C→D, then clearly A∧C→B∧D.
Let's try addition.
+
=
Now, this one is less obvious. Let us interpret A+B to mean A∨B. Can we deduce (A∧D)∨(B∧C)→(B∧D) from A→B and C→D? Indeed we can:
So derivation rules do, in fact, behave a bit like fractions, and by applying some rules from high-school algebra, we can create new, valid rules from given derivations. Weird stuff. 😉
Comments
Zumindest Chromium zeigt die SVGs nicht an, sondern versucht, sie mit einem externen viewer anzuzeigen (also einem Plugin). Ich binde sie immer mit <img /> ein, das ist afaik auch der präferierte weg, wenn man mit ihnen nicht interagieren will.
Okeh, Firefox shows the SVGs correctly.
What you noticed is caused by the fact that types form a commutative semiring (https://en.wikipedia.org/wiki/Semiring). A∧B is essentially the product, and A∨B is the coproduct (or the sum). Semiring axioms are implied by both the ring axioms and the lattice axioms.
However, interpreting the implication as some kind of division is nice. I wonder whether there is more to explore behind this interpretation.
Submit a comment
Note: This website uses a JavaScript-based spam prevention system. Please enable JavaScript in your browser to post comments. Comment format is plain text. Use blank lines to separate paragraphs.