Propositions As Types
MyWikiBiz, Author Your Legacy — Thursday October 31, 2024
Jump to navigationJump to search
Note 1
Identity, or the Identifier Step 1. Given a syntactic specification (or paraphrastic definition): x = xI where "x = x..." is the definiens, or defining context, and "I" is the definiendum, Find a pure interpretant for I, that is, an equivalent term in <<K, S>>, the combinatory algebra generated by K and S, that does as I does. Observe: x = (xK)(xK) = x(K(KS)) => I = K(KS) and so K(KS) constitutes a syntactic algorithm for I. Step 2. Assign types in the specification: x_A = x_A I_(A=>A) to arrive at a propositional typing for I : A => A, whose type, read as a proposition, is a theorem of intuitionistic propositional calculus. Step 3 (optional). Check that A => A is a theorem of classical propositional calculus. A A o---o o---o | | @ = @ = @ Check.
Note 2
Identity, or the Identifier (cont.) Step 4. If we start from the parse tree of the term I in terms of the primitive combinators K and S, that is, the articulation or construction corresponding to the term equation I = (K(KS)), K S o o K \ / o (o) \ / I = (o) , then adding appropriate type-indices to the nodes of this tree will leave us with a proof tree for the propositional type of I : A => A. Thus, the construal or construction of I as K(KS) constitutes a hint or clue to the proof of A => A in the intuitionistic propositional calculus. Although guesswork may succeed in easy cases such as this, a more systematic procedure is to follow the development in Step 1, that takes us from contextual specification to operational algorithm, and to carry along the type information as we go, ending up with a typed parse tree for I, tantamount to a proof tree for A => A.
Note 3
Identity, or the Identifier (cont.) Step 4 (cont.) Term Development: Contextual Definition ~~~> Combinator Construction o-----------------------------------------------------------o | | | x | | (o)A | | | o===========================================================o | | | x K x K | | o A o A=>(B=>A) o A o A=>((B=>A)=>A) | | \ / \ / | | \ / \ / | | (o)B=>A (o)(B=>A)=>A | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | (o)A | | | o===========================================================o | | | K S | | o A=>((B=>A)=>A) o A=>((B=>A)=>A) | | \ / => | | \ / (A=>(B=>A))=>(A=>A) | | \ / | | \ / | | \ / | | \ / | | \ / | | K \ / | | o A=>(B=>A) (o)(A=>(B=>A))=>(A=>A) | | \ / | | \ / | | \ / | | \ / | | \ / | | x \ / | | o A (o)A=>A | | \ / | | \ / | | (o)A | | | o-----------------------------------------------------------o
Note 4
| NB. I am working from rough notes that | I wrote out in the Fall of 1996, and it | is not always easy to reconstruct what | I had in mind at the time. I misread | this passage in my last posting of it, | causing me to leave out a few steps. 1. Identity, or the Identifier (cont.) Step 5. Existential Graph Format, Application Triples with Structure Sharing. Same development in Existential Graph notation. Here I am carrying out the term development in reverse, that is, in application order. o-----------------------------------------------------------o | | | B A B A | | o---o o---o | | | | | | | A A | A x A xI | | o---o o---o o-----o | | | | | | | A | | K | K(KS) = I | | o---o o--------------o | | | | | | | K | KS | | o--------------o | | | | | | S | | @ | | | o===========================================================o | | | B A | | o-----o | | | | | B A | xK A | | o-----o ............[1]---[o](xK)(xK) | | | . | | | A x | xK . A x | xK | | o----[1]........... o-----o | | | | | | | K | K | | @ @ | | | o===========================================================o | | | A | | @ x | | | o-----------------------------------------------------------o | I am still not sure what order I intended for the | application triples, but this is one likely guess: For example: The nodes that are right-labeled <K, KS, K(KS)>, in that order, constitute an application triple. The type of the applicand K is A=>(B=>A). The type of the applicator KS is (A=>(B=>A))=>(A=>A). Therefore, the type of the application K(KS) is A=>A.
Note 5
Composition, or the Composer Step 1. Given a specification of the "composition combinator", or the "composer" P, that has the following effects: x(y(zP)) = (xy)z find an explication of P in terms of primitive combinators. Proceed as follows: (xy)z = (xy)(x(zK)) = x(y((zK)S)) (zK)S = (zK)(z(SK)) = z(K((SK)S)) => x(y(zP)) = (xy)z = x(y(z(K((SK)S)))) => P = (K((SK)S))
Note 6
Composition, or the Composer (cont.) Step 2. Assign types in the specification: B C ((x: y:): z:): A A B B C = B C (A=>B)=>(A=>C) A=>C C (x: (y: (z: P: ): ):): A A B B=>C A=>B A C Here, a notation of the form: x: A means that x is of the type A, while a notation of the form: B x: A means that x is of the type A=>B. Note that the explication of P as a term K((SK)S) of type (B=>C) => ((A=>B)=>(A=>C)) is a clue to the proof of P's type proposition as a theorem of intuitionistic propositional calculus, based on the combinator axioms, K : A => (B=>A) and S : (A=>(B=>C)) => ((A=>B)=>(A=>C)).
Note 7
Composition, or the Composer (cont.) Step 3 (optional). Check that the propositional type of the composer P is a theorem of classical propositional calculus, which is logically necessary to its being a theorem of intuitionistic propositional calculus, but easier to check. o-------------------------------------------------o | | | | | A B A C | | o---o o---o | | | | | | B C | | | | o---o o---------o | | | | | | | | | | o---------o | | | | | | | | @ | | | o=================================================o | | | B C A B | | o---o o---o | | \ / | | \ / | | \ / | | A o---o C | | | | | | | | @ | | | o=================================================o | | | B C B | | o---o o---o | | \ / | | \ / | | \ / | | A o---o C | | | | | | | | @ | | | o=================================================o | | | B o---o C | | | | | | | | AB o---o C | | | | | | | | @ | | | o=================================================o | | | o---o C | | | | | | | | AB o---o C | | | | | | | | @ | | | o=================================================o | | | ABC o---o C | | | | | | | | @ | | | o=================================================o | | | ABC o---o | | | | | | | | @ | | | o=================================================o | | | o---o | | | | | | | | @ | | | o=================================================o | | | @ | | | o-------------------------------------------------o QED.
Note 8
Composition, or the Composer (cont.) Step 4. Repeat the development in Step 1, but this time articulating the type information as we go. o---------------------------------------------------------------------o | | | x y A | | o A o===> | | \ / B | | \ / | | \ / z B | | (o)B o===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | B z K B=>C | | ===>o o===========> | | C \ / A=>(B=>C) | | \ / | | x y A x \ / A | | o A o===> o A (o)=====> | | \ / B \ / B=>C | | \ / \ / | | \ / \ / B | | (o)B (o)===> | | \ / C | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | B z K B=>C | | ===>o o===========> | | C \ / A=>(B=>C) | | \ / | | A \ / S A=>(B=>C) | | =====>(o) o===============> | | B=>C \ / (A=>B)=>(A=>C) | | \ / | | \ / | | \ / | | \ / | | A y \ / A=>B | | ===>o (o)=====> | | B \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | A=>(B=>C) | | ===============> | | A=>(B=>C) S K (A=>B)=>(A=>C) | | ===============>o o==============================> | | (A=>B)=>(A=>C) \ / (B=>C) | | \ / ===============> | | \ / (A=>(B=>C))=>((A=>B)=>(A=>C)) | | \ / | | z B K B=>C z B \ / B=>C | | o===>C o=========> o===> (o)==============================> | | \C / A=>(B=>C) \C / (A=>(B=>C))=>((A=>B)=>(A=>C)) | | \ / \ / | | \ / A \ / A=>(B=>C) | | (o)======> (o)=============> | | \ B=>C / (A=>B)=>(A=>C) | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | A y \ / A=>B | | ===>o (o)======> | | B \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | A=>(B=>C) S K (A=>(B=>C))=>((A=>B)=>(A=>C)) | | =============>o o=======================================> | | (A=>B)=>(A=>C) \ / (B=>C)=>((A=>(B=>C))=>((A=>B)=>(A=>C))) | | \ / | | \ / B=>C | | \ / =========================> | | B=>C \ / S (A=>(B=>C))=>((A=>B)=>(A=>C)) | | ==================>(o) o===============================> | | A=>(B=>C) \ / (B=>C)=>(A=>(B=>C)) | | ===============> \ / =========================> | | (A=>B)=>(A=>C) \ / (B=>C)=>((A=>B)=>(A=>C)) | | \ / | | \ / | | B=>C K \ / (B=>C)=>(A=>(B=>C)) | | ==========>o (o)=========================> | | A=>(B=>C) \ / (B=>C)=>((A=>B)=>(A=>C)) | | \ / | | \ / | | \ / | | \ / | | B z \ / B=>C | | ===>o (o)===============> | | C \ / (A=>B)=>(A=>C) | | \ / | | A y \ / A=>B | | ===>o (o)=====> | | B \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o---------------------------------------------------------------------o
Note 9
Composition, or the Composer (cont.) Step 4 (concl.) The foregoing development has taken us from the typed parse tree for the definiens ((xy)z) to the typed parse tree for the explicated definiendum (x(y(z(K((SK)S)) ))), which gives us both the construction of the composition combinator P in terms of primitive combinators: P = (K((SK)S)) and also the proof tree for the proposition type of P: S K o o \ / S (o) o K \ / o (o) \ / P = (o) P = (K((SK)S)) : (B=>C)=>((A=>B)=>(A=>C))
Note 10
Composition, or the Composer (concl.) Step 5. Rewrite the final proof tree in existential graph format: o-----------------------------------------------------------o | | | B C A B A C | | o--o o--o o--o | | | | | | | B C A B A C A | | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A | | | B C | | | | o--o o-----o o--o o--------o | | | | | | | | | | | | | | o--------o o-----o | | | | | | | S | SK | | o-------------------[1] | | | | | | K | | @ | | | o-----------------------------------------------------------o | | | B C A B A C | | o--o o--o o--o | | | | | | | B C A | B C | | | | o--o o--o o--o o-----o | | | | | | | | | | | | | | o-----o o-----o | | | | | | | K | K((SK)S) = P | | o-------------[o] | | | | | SK | (SK)S | | [1]----o | | | | | | S | | @ | | | o-----------------------------------------------------------o NB. Graphic convention used in the above style of display: Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, amounting in effect to "Facts" being recycled as "Cases". Square brackets are also used to mark the intended result.
Note 11
Self-Documentation Observation. Notice the "self-documenting" property of proof developments in the existential graph format, that is, the property of a developing structure that remembers its own history. For example, the development of the Identity combinator: x = (xK)(xK) = x(K(KS)) o-----------------------------------------------------------o | | | A | | @ | | | | "1" | | | o===========================================================o | | | B A | | o-----o | | | | | B A | A | | o-----o ............[o]----o | | | . | | | A | . A | | | o----[o]........... o-----o | | | | | | | | | | @ @ | | | | "2" "3" | | | o===========================================================o | | | B A B A | | o-----o o-----o | | | | | | | A A | A A | | o-----o o-----o [1]----o | | | | | | | A | | | | | o-----o [2]---------------o | | | | | | | | | | [3]---------------o | | | | | | | | @ | | | o-----------------------------------------------------------o
Note 12
Self-Documentation, Developmental Data Structures (cont.) Redo the entire development of the Composer in existential graph format: Step 5 (extended). o---------------------------------------------------------------------o | Hypotheses: x : A, y : A=>B, z : B=>C | o---------------------------------------------------------------------o | | | (xy)z | | | | A B xy B C (xy)z | | [1]-[2] [2]-[3] | | | | | | A x | y | z | | [1] @ @ | | | o=====================================================================o | | | (xy)(x(zK)) | | | | B C (xy)(x(zK)) | | [2]--o | | | | | B C A | x(zK) | | o---o [1]--o | | | | | | | z | zK | | o------[4] | | | | | | K | | @ | | | o=====================================================================o | | | x(y((zK)S)) | | | | B C A B A C x(y((zK)S)) | | o---o o---o [1]--o | | | | | | | A | | y | y((zK)S) | | o---o o-------o | | | | | | | zK | (zK)S | | [4]----------o | | | | | | S | | @ | | | o=====================================================================o | | | x(y((zK)(z(SK)))) | | | | B C A B A C x(y((zK)(z(SK)))) | | o--o o--o [1]-o | | | | | | | B C A B A C A | | y | y((zK)(z(SK))) | | o--o o--o o--o o--o o-----o | | | | | | | | | A | | | B C | zK | (zK)(z(SK)) | | o--o o-----o o--o [4]-------o | | | | | | | | | | | z | z(SK) | | o--------o o-----o | | | | | | | S | SK | | o-------------------[5] | | | | | | K | | @ | | | o=====================================================================o | | | x(y(z(K((SK)S)))) | | | | B C A B A C B C A B A C | | o--o o--o o--o o--o o--o o--o | | | | | | | | | | A | | | B C A | B C | | | | o--o o-----o o--o o--o o--o o-----o | | | | | | | | | | B C | | | | | | | | o--o o--------o o-----o o-----o | | | | | | | | | | | K | K((SK)S) = P | | o-----o o-------------[o] | | | | | | | SK | (SK)S | | [5]-------------------------o | | | | | | S | | @ | | | o---------------------------------------------------------------------o That's the sketch as best I can reconstruct it from my notes.
Note 13
Triadic Analogy: Analogy Between a Couple of Three-Place Relations o-------------------------------------------------o | | | proof hint : proof : proposition | | | o=================================================o | | | untyped term : typed term : type | | | o-------------------------------------------------o
Note 14
Transposition, or the Transposer x(y(zT)) = y(xz) This equation constitutes a "paraphrastic definition" of T, a definition-in-context, or a formal syntactic specification of how the operator is required to act on other symbols. Step 1. Find a "pure interpretant" for T, that is, an equivalent term doing the job of T which is constructed purely in terms of the primitive combinators K and S. This will constitute an operational algorithm for T, though still operating at the level of abstract syntax, understood as a sequence of manipulations on formal identifiers, or on symbols taken as objects in themselves.
Note 15
Transposition, or the Transposer (cont.) x(y(zT)) = y(xz) Step 1 (concl.) Observe that y(xz) matches (xy)(xz) on the right, and that we can express y as x(yK), consequently: y(xz) = (x(yK))(xz) = x((yK)(zS)) thus completing the abstraction (or disentanglement) of x from the expression. Working on the remainder of the expression, the next item of business is to abstract y. Notice that: (yK)(zS) = (yK)(y((zS)K)) = y(K(((zS)K)S)) thus completing the abstraction of y. Next, work on K(((zS)K)S) to extract z, starting from the center (zS)K of the labyrinth and working outward: (zS)K = (zS)(z(KK)) = z(S((KK)S)) For the sake of brevity in the rest of this development, rename the operator on the right so that (S((KK)S)) = F. Continue with K((zF)S), to extract z: (zF)S = (zF)(z(SK)) = z(F((SK)S)) Rename the operator on the right, letting (F((SK)S)) = G. Continue with K(zG), to extract z: K(zG) = (z(KK))(zG) = z((KK)(GS)) Filling in the abbreviations: y(xz) = x(y(z((KK)(GS)) )) = x(y(z((KK)((F((SK)S))S)) )) = x(y(z((KK)(((S((KK)S))((SK)S))S)) )) Thus we have: T = (KK)(((S((KK)S))((SK)S))S)
Note 16
Transposition, or the Transposer (cont.) Step 2. Using the contextual definition of the transposer T, y(xz) = x(y(zT)), find a minimal generic typing (simplest non-degenerate typing) of each term in the specification that makes all of the applications on each side of the equation go through. For example, here is one such typing: B=>C C B=>C B=>(A=>C) A=>C C (y: (x: z: ): ): = (x: (y: (z: T: ): ): ): B A A B C A B A A=>(B=>C) B A C In a contextual, implicit, or paraphrastic definition of this sort, the "definiendum" is the symbol to be defined, in this case, "T", and the "definiens" is the entire rest of the context, in this case, the frame "y(xz) = x(y(z__))", that ostensibly defines, or as one says, is supposed to define the symbol "T" that we find in its slot. More loosely speaking, the side of the equation with the more known symbols may be called its "defining" side. In order to find a minimal generic typing, start with the defining side of the equation, freely assigning types in such a way that the successive applications make sense, but without introducing unnecessary complications or creating unduly specialized applications. Then work out what the type of the defined operator T has to be, in order to function properly in the standard context, in this case, (x(y(z__))). Again, this gives: B=>C B=>(A=>C) A=>C C B=>C C (x: (y: (z: T: ): ): ): = (y: (x: z: ): ): A B A A=>(B=>C) B A C B A A B C Thus we have T : (A=>(B=>C))=>(B=>(A=>C)), whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.
Note 17
Transposition, or the Transposer (cont.) Step 3 (optional). At this juncture we might want to verify that the proposition corresponding to the type of T is actually a theorem of classical propositional calculus. Since nothing can be a theorem of intuitionistic propositional calculus wihout also being a theorem of classical propositional calculus, this is a necessary condition of our work being correct up to this point. Although it is not a sufficient condition, classical theoremhood is easier to test and so provides a quick and useful check on our work. In existential graph format, T has the following generic typing: o-------------------------------------------------o | | | B C A C | | o--o o--o | | A | B | | | o--o o--o | | | | | | o--------o | | | | | T : @ | | | o-------------------------------------------------o And here is a classical logic proof of the type proposition: o-------------------------------------------------o | | | B C A C | | o--o o--o | | A | B | | | o--o o--o | | | | | | o--------o | | | | | @ | | | o=================================================o | | | AB C AB C | | o--o o--o | | | | | | o--------o | | | | | @ | | | o=================================================o | | | X X | | o--------o | | | | | @ | | | o=================================================o | | | @ | | | o-------------------------------------------------o
Note 18
Transposition, or the Transposer (cont.) Step 4. The construction of the term T of the appropriate type in terms of the primitive typed combinators of the forms K and S is analogous to the proof of the corresponding proposition from the intuitionistic axiom schemes attached to those forms. Incidentally, note the inobtrusive appearance of renaming strategies in the progress of this work. Renaming is the natural operation that substitution is the reverse of. With these humble beginnings we have reached a birthplace, a native ground, of the sign relation, an irreducible three-place relationship among what is indicated, what happens to indicate it, and all of the equivalent or associated indications we may find or create in reference to it. For example, let "G", the interposed interpretant, denote whatever it is, the supposed object, that "(F((SK)S))", the occurrent sign, denotes.
Note 19
Transposition, or the Transposer (cont.) Step 4 (cont.) Consider the following data: The parse tree of the term T = ((KK)(((S((KK)S))((SK)S))S)) and the typing of the term T : (A=>(B=>C))=>(B=>(A=>C)). o-------------------------------------------------o | | | K K | | o o | | \ / S S K | | (o) o o o | | S \ / \ / S | | o (o) (o) o | | \ / \ / | | (o) (o) | | \ / | | \ / | | \ / | | \ / | | K K \ / S | | o o (o) o | | \ / \ / | | (o) (o) | | \ / | | \ / | | \ / | | (o) | | | | (A=>(B=>C))=>(B=>(A=>C)) | | | o-------------------------------------------------o Can proofs be developed by tracing the stepwise articulation or explication of the untyped proof hint, typing each term as we go? For example, we might begin as follows: o-----------------------------------------------------------o | | | B=>C C | | (y: (x: z: ): ): | | B A A B C | | | o===========================================================o | | | A=>B B B=>C C | | ((x: (y: K: ): ): (x: z: ): ): | | A B B A B A A B C | | | o===========================================================o | | | A=>B B B=>C (A=>B)=>(A=>C) A=>C C | | (x: ((y: K: ): (z: S: ): ): ): | | A B B A A A=>(B=>C) A=>B A C | | | o===========================================================o | | | ... | | | o-----------------------------------------------------------o
Note 20
Transposition, or the Transposer (cont.) Step 4 (cont.) If this strategy is successful it suggests that the proof tree can be grown in a stepwise equational fashion from a seed term of the appropriate species, in other words, from a contextual, embedded, or paraphrastic specification of the desired term. Thus, these developments culminate in the rather striking and possibly disconcerting consequence that the apparent flow of information or reasoning in the proof tree is something of a put-up job, a snapshot likeness or a likely story that calls to mind the anatomy of a justification, but fails to reconstruct the true embryology or living physiology of discovery involved.
Note 21
Transposition, or the Transposer (cont.) Step 4 (concl.) Repeat the development in Step 1, but this time articulating the type information as we go. o---------------------------------------------------------------------o | | | x z A | | o A o======> | | \ / B=>C | | \ / | | y \ / B | | o B (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | y K B | | o B o======> | | \ / A=>B | | \ / | | x \ / A x z A | | o A (o)===> o A o======> | | \ / B \ / B=>C | | \ / \ / | | \ / \ / B | | (o)B (o)===> | | \ / C | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | y K B z A S A=>(B=>C) | | o B o=====> o=====> o==============> | | \ / A=>B \B=>C / (A=>B)=>(A=>C) | | \ / \ / | | \ / \ / | | \ / A \ / A=>B | | (o)===> (o)=====> | | \ B / A=>C | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | A z S A=>(B=>C) | | =====>o o==============> | | B=>C \ / (A=>B)=>(A=>C) | | \ / | | A=>B \ / K (A=>B)=>(A=>C) | | =====>(o) o====================> | | B=>C \ / B=>((A=>B)=>(A=>C)) | | \ / | | y K B y \ / B | | o B o=====> o B (o)==============> | | \ / A=>B \ / (A=>B)=>(A=>C) | | \ / \ / | | \ / A \ / A=>B | | (o)===> (o)=====> | | \ B / A=>C | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | A z S A=>(B=>C) | | =====>o o==============> | | B=>C \ / (A=>B)=>(A=>C) | | \ / | | A=>B \ / K (A=>B)=>(A=>C) | | =====>(o) o=====================> | | A=>C \ / B=>((A=>B)=>(A=>C)) | | \ / | | B \ / S B=>((A=>B)=>(A=>C)) | | ===============>(o) o========================> | | (A=>B)=>(A=>C) \ / (B=>(A=>B))=>(B=>(A=>C)) | | \ / | | B K \ / B=>(A=>B) | | =====>o (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | (A=>B)=>(A=>C) | | ======================> | | (A=>B)=>(A=>C) K K B=>((A=>B)=>(A=>C)) | | =====================>o o=======================> | | B=>((A=>B)=>(A=>C)) | / A=>(B=>C) | | | / ======================> | | A z S A=>(B=>C) | / (A=>B)=>(A=>C) | | =====>o o===============> | / =====================> | | B=>C \ | (A=>B)=>(A=>C) | / B=>((A=>B)=>(A=>C)) | | \ | | / | | A=>B \| z A |/ A=>(B=>C) | | =====>(o) o=====> (o)======================> | | A=>C \ \B=>C / (A=>B)=>(A=>C) | | \ \ / =====================> | | \ \ / B=>((A=>B)=>(A=>C)) | | \ \ / | | \ \ /(A=>B)=>(A=>C) | | \ (o)====================> | | \ / B=>((A=>B)=>(A=>C)) | | \ / | | B \ / S B=>((A=>B)=>(A=>C)) | | ===============>(o) o=========================> | | (A=>B)=>(A=>C) \ / (B=>(A=>B))=>(B=>(A=>C)) | | \ / | | B K \ / B=>(A=>B) | | =====>o (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | K K A=>(B=>C) | | o o ======================> | | \ / (A=>B)=>(A=>C) | | \ / =====================> | | A=>(B=>C) \ / S B=>((A=>B)=>(A=>C)) | | ====================>(o) o===================================> | | (A=>B)=>(A=>C) \ | (A=>(B=>C))=>((A=>B)=>(A=>C)) | | =====================> \ | ==================================> | | B=>((A=>B)=>(A=>C)) \ | (A=>(B=>C))=>(B=>((A=>B)=>(A=>C))) | | \ | | | A=>(B=>C) S \| (A=>(B=>C))=>((A=>B)=>(A=>C)) | | ===============>o (o)==================================> | | (A=>B)=>(A=>C) \ / (A=>(B=>C))=>(B=>((A=>B)=>(A=>C))) | | \ / | | A z \ / A=>(B=>C) | | =====>o (o)====================> | | B=>C \ / B=>((A=>B)=>(A=>C)) | | \ / | | B \ / S B=>((A=>B)=>(A=>C)) | | ===============>(o) o=========================> | | (A=>B)=>(A=>C) \ / (B=>(A=>B))=>(B=>(A=>C)) | | \ / | | B K \ / B=>(A=>B) | | =====>o (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | B=>((A=>B)=>(A=>C)) | | ==========================> | | B=>((A=>B)=>(A=>C)) S K (B=>(A=>B))=>(B=>(A=>C)) | | =========================>o o===========================> | | (B=>(A=>B))=>(B=>(A=>C)) \ | A=>(B=>C) | | \ | ==========================> | | K K \ | B=>((A=>B)=>(A=>C)) | | o o \ | =========================> | | \ / S \ | (B=>(A=>B))=>(B=>(A=>C)) | | (o) o \ | | | S \ / \ | | | o (o) \ | | | A z \ / A z \| A=>(B=>C) | | =====>o (o) =====>o (o)==========================> | | B=>C \ | B=>C \ | B=>((A=>B)=>(A=>C)) | | \ | \ | =========================> | | \ | \ | (B=>(A=>B))=>(B=>(A=>C)) | | \ | \ | | | B \| \| B=>((A=>B)=>(A=>C)) | | ===============>(o) (o)========================> | | (A=>B)=>(A=>C) \ / (B=>(A=>B))=>(B=>(A=>C)) | | \ / | | \ / | | \ / | | \ / | | \ / | | B K \ / B=>(A=>B) | | =====>o (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | Define the following abbreviations: | | | | L = M=>N | | | | M = B=>((A=>B)=>(A=>C)) | | | | N = (B=>(A=>B))=>(B=>(A=>C)) | | | | | | S K L | | o L o===============> | | \ / (A=>(B=>C))=>L | | \ / | | A=>(B=>C) \ / S (A=>(B=>C))=>L | | ==========>(o) o================> | | L \ / (A=>(B=>C))=>M | | \ / ===============> | | K K \ / (A=>(B=>C))=>N | | \ / S \ / | | (o) o \ / | | S \ / \ / | | o (o) \ / | | A=>(B=>C) \ / \ / (A=>(B=>C))=>M | | ===========>(o) (o)===============> | | M \ / (A=>(B=>C))=>N | | \ / | | \ / | | \ / | | A z \ / A=>(B=>C) | | =====>o (o)========================> | | B=>C \ / (B=>(A=>B))=>(B=>(A=>C)) | | \ / | | B K \ / B=>(A=>B) | | =====>o (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | K K | | o o | | \ / S S K | | (o) o o o | | S \ / \ / S | | o (o) (o) o | | B K K B=>(A=>B) \ / \ / | | =====>o o===========> (o) (o) | | A=>B \ | A=>(B=>C) \ / | | \ | ==========> \ / | | \ | B=>(A=>B) \ / | | \ | \ / | | A z \| A=>(B=>C) z A \ / A=>(B=>C) | | =====>o (o)==========> o=====> (o)========================> | | B=>C \ | B=>(A=>B) \B=>C / (B=>(A=>B))=>(B=>(A=>C)) | | \ | \ / | | \ | \ / | | B \| \ / B=>(A=>B) | | =====>(o) (o)==========> | | A=>B \ / B=>(A=>C) | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o=====================================================================o | | | K K | | o o | | \ / S S K | | (o) o o o | | S \ / \ / S | | o (o) (o) o | | \ / \ / | | (o) (o) | | \ / | | \ / | | \ / A=>(B=>C) | | \ / =========================> | | A=>(B=>C) \ / S (B=>(A=>B))=>(B=>(A=>C)) | | =========================>(o) o==========================> | | (B=>(A=>B))=>(B=>(A=>C)) | / (A=>(B=>C))=>(B=>(A=>B)) | | | / =========================> | | B K K B=>(A=>B) | / (A=>(B=>C))=>(B=>(A=>C)) | | =====>o o===========> | / | | A=>B \ | A=>(B=>C) | / | | \ | ==========> | / | | \ | B=>(A=>B) | / | | A=>(B=>C) \| |/ (A=>(B=>C))=>(B=>(A=>B)) | | ==========>(o) (o)=========================> | | B=>(A=>B) \ / (A=>(B=>C))=>(B=>(A=>C)) | | \ / | | \ / | | \ / | | \ / | | \ / | | A z \T/ A=>(B=>C) | | =====>o (o)==========> | | B=>C \ / B=>(A=>C) | | \ / | | y \ / B | | o B (o)=====> | | \ / A=>C | | \ / | | x \ / A | | o A (o)===> | | \ / C | | \ / | | \ / | | (o)C | | | o---------------------------------------------------------------------o
Note 22
Transposition, or the Transposer (cont.) Step 5. Rewrite the final proof tree in existential graph format, implementing structure sharing among application triples by overlaying the type propositions that attach to terms. Graphic Conventions: Square bracketed nodes mark subtrees to be pruned from one tree and grafted into another at the indicated site, tantamount to recycling "Facts" as "Cases". Square brackets are also used to indicate the final result. o---------------------------------------------------------------------o | | | A B A C | | o--o o--o | | | | | | A B A C A B A C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A B A C | | B C | | B | | | o--o o--o o-----o o--o o-----o o--o | | | | | | | | | | | | B | A | | | | | o-----o o--o o--o o-----------o | | | | | | | | | | | | | | o-----------o o--------o | | | | | | | K | KK | | o-------------------------[1] | | | | | | K | | @ | | | o---------------------------------------------------------------------o | | | A B A C | | o--o o--o | | | | | | B C A B A C B C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A | | | A | B | | | o--o o-----o o--o o--o | | | | | | | | | | | | | | o--------o o----------o | | | | | | | S | S((KK)S) | | o-------------------[2] | | | | | KK | (KK)S | | [1]----o | | | | | | S | | @ | | | o---------------------------------------------------------------------o | | | A B A C A B A C | | o--o o--o o--o o--o | | | | | | | | A B A C A B A C | | B | B | | | o--o o--o o--o o--o o-----o o--o o--o | | | | | | | | | | | | | B | B | B C B | | | | | o-----o o--o o--o o--o o--o o------o | | | | | | | | | | B | | | A | | | | | o--o o------o o--o o------------o | | | | | | | | | | | | | | o------------o o--------o | | | | | | | S | SK | | o-------------------------[3] | | | | | | K | | @ | | | o---------------------------------------------------------------------o | | | A B A C | | o--o o--o | | | | | | B C B | B | | | o--o o--o o--o | | | | | | | A | | | | | o--o o--------o | | | | | | | | | | o--------o | | | | | S((KK)S) | (S((KK)S))((SK)S) | | [2]---------[4] | | | | | SK | (SK)S | | [3]----------o | | | | | | S | | @ | | | o---------------------------------------------------------------------o | | | B C A B | | o--o o--o | | | | | | A B A | B | | | o--o o--o o--o | | | | | | | B | | | | | o--o o--------o | | | | | | | K | KK | | o-------[5] | | | | | | K | | @ | | | o---------------------------------------------------------------------o | | | T = (KK)(((S((KK)S))((SK)S))S) | | | | B C A C | | o--o o--o | | | | | | A | B | | | o--o o--o | | | | | | | | | | o--------o | | | | | KK | T | | [5]------------------[o] | | | | | (S((KK)S))((SK)S) | ((S((KK)S))((SK)S))S | | [4]-------------------o | | | | | | S | | @ | | | o---------------------------------------------------------------------o
Note 23
Transposition, or the Transposer (cont.) Step 5 (extended). Redo the development of the proof tree in existential graph format. Each frame of the developmental scheme that follows is divided by a dotted line, with terms that contribute to the main term under development being shown above it and the main term itself being shown below it. o---------------------------------------------------------------------o | Hypotheses: x : A, y : B, z : A=>(B=>C) | o---------------------------------------------------------------------o | | | y(xz) | | | | A x | | [1] | | | | B y | | [2] | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | B C y(xz) | | [2]--o | | | | | A | xz | | [1]--o | | | | | | z | | @ | | | o=====================================================================o | | | (x(yK))(xz) | | | | A B x(yK) | | o--[3] | | | | | B | yK | | o---o | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | B C (x(yK))(xz) | | [3]--o | | | | | A | xz | | o---o | | | | | | z | | @ | | | o=====================================================================o | | | x((yK)(zS)) | | | | A B | | o---o | | | | | B | yK | | o--[4] | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | B C A B A C x((yK)(zS)) | | o---o o---o o---o | | | | | | | A | | yK | (yK)(zS) | | o---o [4]------o | | | | | | | z | zS | | o-----------o | | | | | | S | | @ | | | o=====================================================================o | | | x((yK)(y((zS)K))) | | | | A B | | o---o | | | | | B | yK | | o--[4] | | | | | | K | | @ | | | | B C A B A C | | o---o o---o o---o | | | | | | | A | | | | | o---o o-------o | | | | | | | z | zS | | o----------[5] | | | | | | S | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C x((yK)(y((zS)K))) | | o---o o---o | | | | | | A B A C | yK | (yK)(y((zS)K)) | | o---o o---o [4]------o | | | | | | | | | B | y((zS)K) | | o-------o o---o | | | | | | | zS | (zS)K | | [5]--------------o | | | | | | K | | @ | | | o=====================================================================o | | | x(y(K(((zS)K)S))) | | | | B C A B A C | | o---o o---o o---o | | | | | | | A | | | | | o---o o-------o | | | | | | | z | zS | | o----------[5] | | | | | | S | | @ | | | | A B A C | | o---o o---o | | | | | | A B A C | | | | o---o o---o o-------o | | | | | | | | | B | | | o-------o o---o | | | | | | | zS | (zS)K | | [5]-------------[6] | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C A B A C x(y(K(((zS)K)S))) | | o---o o---o o---o o---o | | | | | | | | | | B | B | y(K(((zS)K)S)) | | o-------o o---o o---o | | | | | | | B | | K | K(((zS)K)S) | | o---o o----------o | | | | | | | (zS)K | ((zS)K)S | | [6]-----------------o | | | | | | S | | @ | | | o=====================================================================o | | | x(y(K(((zS)(z(KK)))S))) | | | | B C A B A C | | o--o o--o o--o | | | | | | | A | | | | | o--o o-----o | | | | | | | z | zS | | o-------[5] | | | | | | S | | @ | | | | A B A C | | o--o o--o | | | | | | A B A C A B A C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A B A C | | B C | | B | | | o--o o--o o-----o o--o o-----o o--o | | | | | | | | | | | | B | A | | zS | (zS)(z(KK)) | | o-----o o--o o--o [5]---------[7] | | | | | | | | | | | z | z(KK) | | o-----------o o--------o | | | | | | | K | KK | | o--------------------------o | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C A B A C | | o--o o--o o--o o--o x(y(K(((zS)(z(KK)))S))) | | | | | | | | | | B | B | y(K(((zS)(z(KK)))S)) | | o-----o o--o o--o | | | | | | | B | | K | K(((zS)(z(KK)))S) | | o--o o---------o | | | | | | | (zS)(z(KK)) | ((zS)(z(KK)))S | | [7]--------------o | | | | | | S | | @ | | | o=====================================================================o | | | x(y(K((z(S((KK)S)))S))) | | | | A B A C | | o--o o--o | | | | | | A B A C A B A C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A B A C | | B C | | B | | | o--o o--o o-----o o--o o-----o o--o | | | | | | | | | | | | B | A | | | | | o-----o o--o o--o o-----------o | | | | | | | | | | | | | | o-----------o o--------o | | | | | | | K | KK | | o-------------------------[8] | | | | | | K | | @ | | | | A B A C A B A C | | o-o o-o o-o o-o | | | | | | | | A B A C | | B C A B A C B C | | | | o-o o-o o----o o-o o-o o-o o-o o----o | | | | | | | | | | | | B C | | B | A | | | A | B | | | o-o o----o o-o o-o o----o o-o o-o | | | | | | | | | | | A | | | | | | z | z(S((KK)S)) | | o-o o--------o o------o o----[9] | | | | | | | | | | | S | S((KK)S) | | o------o o---------------o | | | | | | | KK | (KK)S | | [8]-------------------------o | | | | | | S | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C A B A C x(y(K((z(S((KK)S)))S))) | | o--o o--o o--o o--o | | | | | | | | | | B | B | y(K((z(S((KK)S)))S)) | | o-----o o--o o--o | | | | | | | B | | K | K((z(S((KK)S)))S) | | o--o o--------o | | | | | | | z(S((KK)S)) | (z(S((KK)S)))S | | [9]--------------o | | | | | | S | | @ | | | o=====================================================================o | | | x(y(K((z(S((KK)S)))(z(SK))))) | | | | A B A C | | o--o o--o | | | | | | A B A C A B A C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A B A C | | B C | | B | | | o--o o--o o-----o o--o o-----o o--o | | | | | | | | | | | | B | A | | | | | o-----o o--o o--o o-----------o | | | | | | | | | | | | | | o-----------o o--------o | | | | | | | K | KK | | o-------------------------[8] | | | | | | K | | @ | | | | A B A C A B A C | | o-o o-o o-o o-o | | | | | | | | A B A C | | B C A B A C B C | | | | o-o o-o o----o o-o o-o o-o o-o o----o | | | | | | | | | | | | B C | | B | A | | | A | B | | | o-o o----o o-o o-o o----o o-o o-o | | | | | | | | | | | A | | | | | | z | z(S((KK)S)) | | o-o o--------o o------o o----[9] | | | | | | | | | | | S | S((KK)S) | | o------o o---------------o | | | | | | | KK | (KK)S | | [8]-------------------------o | | | | | | S | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | x(y(K((z(S((KK)S)))(z(SK))))) | | ^ | | A B A C A B A C | | | o-o o-o o-o o-o | | | | | | | | A B A C A B A C | | B | B | | | o-o o-o o-o o-o o---o o-o o-o | | | | | | | | | | | | | B | B | B C B | | K | K((z(S((KK)S)))(z(SK))) | | o---o o-o o-o o-o o-o o----o | | | | | | | | | | B | | | A | | | (z(S((KK)S)))(z(SK)) | | o-o o----o o-o [9]-------o | | | | | | | | | | | z | z(SK) | | o--------o o-----o | | | | | | | S | SK | | o------------------o | | | | | | K | | @ [9] = z(S((KK)S)) | | | o=====================================================================o | | | x(y(K(z((S((KK)S))((SK)S))))) | | | | A B A C | | o--o o--o | | | | | | A B A C A B A C | | | | o--o o--o o--o o--o o-----o | | | | | | | | | A B A C | | B C | | B | | | o--o o--o o-----o o--o o-----o o--o | | | | | | | | | | | | B | A | | | | | o-----o o--o o--o o-----------o | | | | | | | | | | | | | | o-----------o o--------o | | | | | | | K | KK | | o-------------------------[8] | | | | | | K | | @ | | | | A B A C A B A C | | o-o o-o o-o o-o | | | | | | | | A B A C | | B C A B A C B C | | | | o-o o-o o----o o-o o-o o-o o-o o----o | | | | | | | | | | | | B C | | B | A | | | A | B | | | o-o o----o o-o o-o o----o o-o o-o | | | | | | | | | | | A | | | | | | | | | o-o o--------o o------o o-----o | | | | | | | | | | | S | S((KK)S) | | o------o o-------------[10] | | | | | | | KK | (KK)S | | [8]-------------------------o | | | | | | S | | @ | | | | A B A C A B A C | | o-o o-o o-o o-o | | | | | | | | A B A C A B A C | | B | B | | | o-o o-o o-o o-o o---o o-o o-o | | | | | | | | | | | | | B | B | B C B | | | | | o---o o-o o-o o-o o-o o----o | | | | | | | | | | B | | | A | | | | | o-o o----o o-o o--------o | | | | | | | | | | | | | | o--------o o-----o | | | | | | | S | SK | | o----------------[11] | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C A B A C A B A C A B A C x(y(K(zG))) | | o-o o-o o-o o-o o-o o-o o-o o-o | | | | | | | | | | | | | | B | B | B C | | B C B | B | y(K(zG)) | | o---o o-o o-o o-o o---o o-o o-o o-o | | | | | | | | | | | | B C B | | | A | B | A | | K | K(zG) | | o-o o-o o----o o-o o-o o-o o----o | | | | | | | | | | | A | | | | | | z | zG | | o-o o--------o o----o o-----o | | | | | | | | | | | F | G | | o-----o [10]---------o | | | | | | | SK | (SK)S | | [11]--------------------o | | | | | | S F = S((KK)S) | | @ G = F((SK)S) = (S((KK)S))((SK)S) | | | o=====================================================================o | | | x(y((z(KK))(z((S((KK)S))((SK)S))))) | | | | B C A B | | o---o o---o | | | | | | A B A | B | | | o---o o---o o---o | | | | | | | B | | z | z(KK) | | o---o o---------[12] | | | | | | | K | KK | | o-----------o | | | | | | K | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | x(y((z(KK))(zG))) | | ^ | | A B A C A B A C A B A C A B A C | | | o-o o-o o-o o-o o-o o-o o-o o-o | | | | | | | | | | | | | | B | B | B C | | B C B | B | y((z(KK))(zG)) | | o---o o-o o-o o-o o---o o-o o-o o-o | | | | | | | | | | | | B C B | | | A | B | A | | | (z(KK))(zG) | | o-o o-o o----o o-o o-o o-o [12]--o | | | | | | | | | | | A | | | | | | z | zG | | o-o o--------o o----o o-----o | | | | | | | | | | | F | G | | o-----o o-----------o | | | | | | | SK | (SK)S | | o----------------------o | | | | | | S F = S((KK)S) | | @ G = F((SK)S) = (S((KK)S))((SK)S) | | | o=====================================================================o | | | x(y(z((KK)(((S((KK)S))((SK)S))S)))) | | | | B C A B | | o---o o---o | | | | | | A B A | B | | | o---o o---o o---o | | | | | | | B | | | | | o---o o-----------o | | | | | | | K | KK | | o---------[13] | | | | | | K | | @ | | | | A B A C A B A C A B A C A B A C | | o-o o-o o-o o-o o-o o-o o-o o-o | | | | | | | | | | | | | | B | B | B C | | B C B | B | | | o---o o-o o-o o-o o---o o-o o-o o-o | | | | | | | | | | | | B C B | | | A | B | A | | | | | o-o o-o o-----o o-o o-o o-o o-----o | | | | | | | | | | | A | | | | | | | | | o-o o---------o o-----o o-----o | | | | | | | | | | | S((KK)S) | (S((KK)S))((SK)S) | | o-----o o-------------[14] | | | | | | | SK | (SK)S | | o--------------------------o | | | | | | S | | @ | | | | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | | | | A B A C B C A B B C A C | | o--o o--o o--o o--o o--o o--o | | | | | | | | | | B C B | B | A | B | A | B | | | o--o o--o o--o o--o o--o o--o o--o | | | | | | | | | | | A | | | | | | | | | o--o o--------o o--------o o--------o | | | | | | | | | | | KK | T | | o--------o [13]--------------[o] | | | | | | | (S((KK)S))((SK)S) | ((S((KK)S))((SK)S))S | | [14]------------------------o | | | | | | S | | @ T = (KK)(((S((KK)S))((SK)S))S) | | | o---------------------------------------------------------------------o <pre> o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types -- Commentary o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Commentary Note 1 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o I think it's best to begin with a few simple observations, as I frequently find it necessary to return to the basics again and again, even if I take a different path each time. Observation 1 If we have the information that an element x is constrained to be of the type X and we have the information that a function f is constrained to be of the type X -> Y then we have the information that the element f(x) is constrained to be of the type Y. We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form: x : X f : X -> Y ----------- f(x) : Y In this scheme of inference, the notations "x", "f", and "f(x)" are taken to be names of formal objects. Some people will call these notations by the name of "terms", while other people will somewhat more confusedly say that the formal objects themselves are the terms. Because it is so important to distinguish signs denoting from objects denoted, I will make some effort to avoid the latter usage, and recommend sticking with the first option. In the same context, the notations "X", "X -> Y", and "Y" give us information, or indicate formal constraints, that we may think of as denoting the "types" of the formal objects under consideration. By an act of "hypostatic abstraction", one may of course elect to view these types as a species of formal objects existing in their own right, inhabiting their own niche, as it were. If a moment's spell of double vision leads us to see the functional arrow "->" as the logical arrow "=>", then we may observe that the right side of this inference scheme follows the pattern of logical deduction that is usually called "modus ponens". And so we forge a tentative link between the pattern of information conversion implicated in functional application and the pattern of information conversion involved in the logical rule of modus ponens. o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Commentary Note 2 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o Re: PAT. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872 Notice that I am carrying out combinator applications "on the right", so the formulas might be backwards from what many people are used to. Here are a three references on combinatory logic and lambda calculus, given in order of difficulty from introductory to advanced, that are especially pertinent to the use of combinators in computer science: | Smullyan, R., |'To Mock a Mockingbird, And Other Logic Puzzles, | Including an Amazing Adventure in Combinatory Logic', | Alfred A. Knopf, New York, NY, 1985. | Hindley, J.R. and Seldin, J.P., |'Introduction to Combinators and [Lambda]-Calculus', | London Mathematical Society Student Texts No. 1, | Cambridge University Press, Cambridge, UK, 1986. | Lambek, J. and Scott, P.J., |'Introduction To Higher Order Categorical Logic', | Cambridge University Press, Cambridge, UK, 1986. | http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521356539 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Commentary Note 3 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Work Area o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o I have been posting excerpts to the ONT List, between note_01 & note_30: note_01 = http://suo.ieee.org/ontology/msg03373.html note_30 = http://suo.ieee.org/ontology/msg03418.html Here is a synopsis, exhibiting just the layering of axioms -- notice the technique of starting over at the initial point several times and building up both more richness of detail and more generality of perspective with each passing time: Concrete Category | Definition 1.1. A 'concrete category' is a collection of two kinds | of entities, called 'objects' and 'morphisms'. The former are sets | which are endowed with some kind of structure, and the latter are | mappings, that is, functions from one object to another, in some | sense preserving that structure. Among the morphisms, there is | attached to each object A the 'identity mapping' 1_A : A -> A | such that 1_A(a) = a for all a in A. Moreover, morphisms | f : A -> B and g : B -> C may be 'composed' to produce | a morphism gf : A -> C such that (gf)(a) = g(f(a)) | for all a in A. | We shall now progress from concrete categories | to abstract ones, in three easy stages. Graph | Definition 1.2. A 'graph' (usually called a 'directed graph') consists | of two classes: the class of 'arrows' (or 'oriented edges') and the class | of 'objects' (usually called 'nodes' or 'vertices') and two mappings from | the class of arrows to the class of objects, called 'source' and 'target' | (often also 'domain' and 'codomain'). | | o--------------o source o--------------o | | | ----------------> | | | | Arrows | | Objects | | | | ----------------> | | | o--------------o target o--------------o | | One writes "f : A -> B" for "source f = A and target f = B". | A graph is said to be 'small' if the classes of objects and | arrows are sets. Deductive System | A 'deductive system' is a graph in which to each object A there | is associated an arrow 1_A : A -> A, the 'identity' arrow, and to | each pair of arrows f : A -> B and g : B -> C there is associated | an arrow gf : A -> C, the 'composition' of f with g. A logician | may think of the objects as 'formulas' and of the arrows as | 'deductions' or 'proofs', hence of | | f : A -> B g : B -> C | --------------------------- | gf : A -> C | | as a 'rule of inference'. Category | A 'category' is a deductive system in which the following equations hold, | for all f : A -> B, g : B -> C, and h : C -> D. | | f 1_A = f = 1_B f, | | (hg)f = h(gf). Functor | Definition 1.3. A 'functor' F : $A$ -> $B$ is | first of all a morphism of graphs (see Example C4), | that is, it sends objects of $A$ to objects of $B$ | and arrows of $A$ to arrows of $B$ such that, if | f : A -> A', then F(f) : F(A) -> F(A'). Moreover, | a functor preserves identities and composition; | thus: | | F(1_A) = 1_F(A), | | F(gf) = F(g)F(f). | | In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves | objects and arrows unchanged and the composition of functors | F : $A$ -> $B$ and G : $B$ -> $C$ is given by: | | (GF)(A) = G(F(A)), | | (GF)(f) = G(F(f)), | | for all objects A of $A$ and all arrows f : A -> A' in $A$. Natural Transformation | Definition 2.1. Given functors F, G : $A$ -> $B$, | a 'natural transformation' t : F -> G is a family | of arrows t(A) : F(A) -> G(A) in $B$, one arrow for | each object A of $A$, such that the following square | commutes for all arrows f : A -> B in $A$: | | t(A) | F(A) o------------------>o G(A) | | | | | | | F(f) | | G(f) | | | | v v | F(B) o------------------>o G(B) | t(B) | | that is to say, such that | | G(f)t(A) = t(B)F(f). Graph | We recall (Part 0, Definition 1.2) that, for categories, | a 'graph' consists of two classes and two mappings | between them: | | o--------------o source o--------------o | | | ----------------> | | | | Arrows | | Objects | | | | ----------------> | | | o--------------o target o--------------o | | In graph theory the arrows are usually called "oriented edges" | and the objects "nodes" or "vertices", but in various branches | of mathematics other words may be used. Instead of writing | | source(f) = A, | | target(f) = B, | f | one often writes f : A -> B or A ---> B. We shall | look at graphs with additional structure which are | of interest in logic. Deductive System | A 'deductive system' is a graph with a specified arrow | | 1_A | R1a. A -----> A, | | and a binary operation on arrows ('composition') | | f g | A ---> B B ---> C | R1b. ---------------------- | gf | A ----> C Conjunction Calculus | A 'conjunction calculus' is a deductive system dealing with truth and | conjunction. Thus we assume that there is given a formula 'T' (= true) | and a binary operation '&' (= and) for forming the conjunction A & B of | two given formulas A and B. Moreover, we specify the following additional | arrows and rules of inference: | | O_A | R2. A -----> T, | | p1_A,B | R3a. A & B --------> A, | | p2_A,B | R3b. A & B --------> B, | | f g | C ---> A C ---> B | R3c. ----------------------. | <f, g> | C --------> A & B Positive Intuitionistic Propositional Calculus | A 'positive intuitionistic propositional calculus' is a conjunction calculus | with an additional binary operation '<=' (= if). Thus, if A and B are formulas, | so are T, A & B, and A <= B. (Yes, most people write B => A instead.) We also | specify the following new arrow and rule of inference: | | !e!_A,B | R4a. (A <= B) & B ---------> A, | | h | C & B ---> A | R4b. ----------------. | h* | C ----> A <= B | Intuitionistic Propositional Calculus | An 'intuitionistic propositional calculus' is more than a | positive one; it requires also falsehood and disjunction, | that is, a formula 'F' (= false) and an operation 'v' (= or) | on formulas, together with the following additional arrows: | | []_A | R5. F ------> A, | | k1_A,B | R6a. A --------> A v B, | | k2_A,B | R6b. B --------> A v B, | | !z!^C_A,B | R6c. (C <= A) & (C <= B) -----------> C <= (A v B). Classical Propositional Calculus | If we want 'classical' propositional logic, we must also require: | | R7. F <= (F <= A) -> A. Category | A 'category' is a deductive system in which | the following equations hold between proofs: | | E1. f 1_A = f, | | 1_B f = f, | | (hg)f = h(gf), | | for all f : A -> B, g : B -> C, h : C -> D. Cartesian Category | A 'cartesian category' is both a category | and a conjunction calculus satisfying the | additional equations: | | E2. f = O_A, for all f : A -> T. | | E3a. p1_A,B <f, g> = f, | | E3b. p2_A,B <f, g> = g, | | E3c. <p1_A,B h, p2_A,B h> = h, | | for all f : C -> A, g : C -> B, h : C -> A & B. Cartesian Closed Category | A 'cartesian closed category' is a cartesian category $A$ with | additional structure R4 satisfying the additional equations: | | E4a. !e!_A,B <h* p1_C,B, p2_C,B> = h, | | E4b. (!e!_A,B <k p1_C,B, p2_C,B>)* = k, | | for all h : C & B -> A, k : C -> (A <= B). | | Thus, a cartesian closed category is | a positive intuitionistic propositional | calculus satisfying the equations E1 to E4. | This illustrates the general principle that | one may obtain interesting categories from | deductive systems by imposing an appropriate | equivalence relation on proofs. o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types -- 2004 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types A Inquiry List 00. http://stderr.org/pipermail/inquiry/2004-June/thread.html#1643 00. http://stderr.org/pipermail/inquiry/2004-July/thread.html#1677 01. http://stderr.org/pipermail/inquiry/2004-June/001643.html 02. http://stderr.org/pipermail/inquiry/2004-June/001644.html 03. http://stderr.org/pipermail/inquiry/2004-June/001645.html 04. http://stderr.org/pipermail/inquiry/2004-June/001660.html 05. http://stderr.org/pipermail/inquiry/2004-June/001648.html 06. http://stderr.org/pipermail/inquiry/2004-June/001649.html 07. http://stderr.org/pipermail/inquiry/2004-June/001656.html 08. http://stderr.org/pipermail/inquiry/2004-June/001657.html 09. http://stderr.org/pipermail/inquiry/2004-June/001658.html 10. http://stderr.org/pipermail/inquiry/2004-June/001659.html 11. http://stderr.org/pipermail/inquiry/2004-June/001661.html 12. http://stderr.org/pipermail/inquiry/2004-June/001662.html 13. http://stderr.org/pipermail/inquiry/2004-June/001664.html 14. http://stderr.org/pipermail/inquiry/2004-June/001665.html 15. http://stderr.org/pipermail/inquiry/2004-June/001666.html 16. http://stderr.org/pipermail/inquiry/2004-June/001667.html 17. http://stderr.org/pipermail/inquiry/2004-June/001668.html 18. http://stderr.org/pipermail/inquiry/2004-June/001670.html 19. http://stderr.org/pipermail/inquiry/2004-June/001671.html 20. http://stderr.org/pipermail/inquiry/2004-June/001672.html 21. http://stderr.org/pipermail/inquiry/2004-June/001673.html 22. http://stderr.org/pipermail/inquiry/2004-June/001674.html 23. http://stderr.org/pipermail/inquiry/2004-July/001677.html o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types B Inquiry List 00. http://stderr.org/pipermail/inquiry/2004-June/thread.html#1647 00. http://stderr.org/pipermail/inquiry/2004-July/thread.html#1684 01. http://stderr.org/pipermail/inquiry/2004-June/001647.html 02. http://stderr.org/pipermail/inquiry/2004-June/001663.html 03. http://stderr.org/pipermail/inquiry/2004-June/001669.html 04. http://stderr.org/pipermail/inquiry/2004-July/001684.html NKS Forum 00. http://forum.wolframscience.com/showthread.php?threadid=490 01. http://forum.wolframscience.com/showthread.php?postid=1517#post1517 02. http://forum.wolframscience.com/showthread.php?postid=1548#post1548 03. http://forum.wolframscience.com/showthread.php?postid=1550#post1550 04. http://forum.wolframscience.com/showthread.php?postid=1590#post1590 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types -- 2005 o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o PAT. Propositions As Types 00. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2872 01. http://stderr.org/pipermail/inquiry/2005-July/002872.html 02. http://stderr.org/pipermail/inquiry/2005-July/002873.html 03. http://stderr.org/pipermail/inquiry/2005-July/002874.html 04. http://stderr.org/pipermail/inquiry/2005-July/002875.html 05. http://stderr.org/pipermail/inquiry/2005-July/002876.html 06. http://stderr.org/pipermail/inquiry/2005-July/002877.html 07. http://stderr.org/pipermail/inquiry/2005-July/002878.html 08. http://stderr.org/pipermail/inquiry/2005-July/002879.html 09. http://stderr.org/pipermail/inquiry/2005-July/002880.html 10. http://stderr.org/pipermail/inquiry/2005-July/002881.html 11. http://stderr.org/pipermail/inquiry/2005-July/002882.html 12. http://stderr.org/pipermail/inquiry/2005-July/002883.html 13. http://stderr.org/pipermail/inquiry/2005-July/002884.html 14. http://stderr.org/pipermail/inquiry/2005-July/002885.html 15. http://stderr.org/pipermail/inquiry/2005-July/002886.html 16. http://stderr.org/pipermail/inquiry/2005-July/002887.html 17. http://stderr.org/pipermail/inquiry/2005-July/002888.html 18. http://stderr.org/pipermail/inquiry/2005-July/002889.html 19. http://stderr.org/pipermail/inquiry/2005-July/002890.html 20. http://stderr.org/pipermail/inquiry/2005-July/002891.html 21. http://stderr.org/pipermail/inquiry/2005-July/002892.html 22. http://stderr.org/pipermail/inquiry/2005-July/002893.html 23. http://stderr.org/pipermail/inquiry/2005-July/002894.html PAT. Propositions As Types -- Commentary 00. http://stderr.org/pipermail/inquiry/2005-July/thread.html#2895 01. http://stderr.org/pipermail/inquiry/2005-July/002895.html 02. http://stderr.org/pipermail/inquiry/2005-July/002896.html 03. o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o