[Inquiry] Re: Propositions As Types -- Series A
Jon Awbrey
jawbrey at att.net
Mon Jun 28 22:24:05 CDT 2004
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note A21
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
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-------------------------------< QEI >-------------------------------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