Day 20: This, That, and These
Composing signs from other signs is a fundamental strategy for managing the complexity of non-trivial communication, regarding complex signs at one level as individual signs at a higher level.
(Goguen 1998, 3 ))
Today’s Progress
PLT
- Finished implementing all the most generally useful parts of
Data.TheseandData.Alignin OCaml. - I spent some time researching, thinking, and taking notes on a semiotic analysis of λ-calculus. The ultimate aim of this line of thinking is to see if I can use Goguen’s methodology of algebraic semiotics (see (Goguen 1998)) to represent type systems as “semiotic morphisms” from the untyped λ-calculus. This follows a suspicion that, for type systems on the left side of the λ-cube (where types never depend on terms) type systems can be understood as interfaces to the λ-calculus. (This must, naturally, proceed on a view typing ala-Curry, since in the Church approach the typing is embedded in the lambda terms).
Tomorrow’s Program
PLT
Write the test suite for the OCaml port of These and the nascent Alg library,
providing algebraic data structures.
Writing
Spend some time collecting my thoughts on the speculative convergence of semiotics (in the tradition of Peirce advaced by Goguen) with some of Girard’s writing in (Girard 2011) and the concern with communication and community in Nancy’s (by Peter Connor 2001).
References
Girard, Jean-Yves. 2011. The Blind Spot : Lectures on Logic. European Mathematical Society. http://www.worldcat.org/oclc/757486610?referer=xid.
Goguen, Joseph. 1998. “An Introduction to Algebraic Semiotics, with Application to User Interface Design.” In International Workshop on Computation for Metaphors, Analogy, and Agents, 242–91. Springer.
Peter Connor, Jean-Luc Nancy; Ed. by. 2001. The Inoperative Community. University of Minnesota Press. http://www.worldcat.org/oclc/402523364?referer=xid.