Containers, monads and induction recursion

Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a setUofcodesand a decoding functionT : U → Dwhich assigns to every codeu : U, a valueT, uof some typeD, e.g.the large type Set of small types or sets. The name induction recursion refers to the build-up of codes inUusing inductive clauses, simultaneously with the definition of the functionT, by structural recursion on codes.Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation – in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.

ACTIVE TILE SELF-ASSEMBLY, PART 2: SELF-SIMILAR STRUCTURES AND STRUCTURAL RECURSION

We introduce a mathematical framework to describe self-similarity and structural recursion within the active tile self-assembly model, thereby providing a connection between substitution tiling and algorithmic self-assembly. We show that one such structurally recursive assembly system can simulate the dynamics of the self-similar substitution tiling known as the L-shape tiling.