[Inquiry] Re: Propositions As Types -- Series A
Jon Awbrey
jawbrey at att.net
Tue Jun 22 23:50:48 CDT 2004
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note A8
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
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
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
More information about the Inquiry
mailing list