2008 January 30 – 3:29 pm
In linear lambda calculus, you must use each bound variable exactly once in a term. A term with a single bound variable is a full binary tree of applications in which one of the leaves is the bound variable, so it makes sense to ask, “which leaf?”
Three combinators are universal for the free linear [...]
2008 January 26 – 2:46 pm
Consider the problem of how to represent negation of a proposition when we only have implication and falsehood:
Since is true and is false, this does what we want.
The contrapositive says has the same truth value as Using only implication, the contrapositive of is
What if we don’t even have [...]
2008 January 17 – 1:16 pm
The category GraphUp of graphs and Granovetter update rules has
directed finite graphs as objects
morphisms generated by Granovetter rules, i.e. the following five operations:
add a new node. (creation, refcount=0)
given a node add a new node and an edge (creation, refcount=1)
given edges and add an edge (introduction, ++refcount)
remove an edge. (deletion, [...]
where is either an input channel or an output channel and is taken from a countably infinite set.
Structural congruence:
[with replacing ] if does not appear in (alpha conversion)
(parallel processes)
(association)
(restriction)
(replication)
if is not free in
Reduction rules:
[with replacing ]
If [...]
A monad in Haskell is about composing almost-compatible morphisms. Typically you’ve got some morphism and then you think of a reason that you’d rather have where is a functor. In Haskell, though, you don’t define functors right out: you define type constructors, which are like the map of objects in [...]
