Tree Calculus

The draft of my book “Reflective Programs in Tree Calculus” is now available for comment at https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf Some front-matter is available from https://github.com/barry-jay-personal/tree-calculus/blob/master/tweets_on_trees.pdf

It may be of interest for two reasons:

  • all proofs have been verified in Coq, and
  • the subject matter will be of interest to those who care about foundations.

Tree calculus programs are combinations built from a single operator that satisfies three equations without side-conditions. As well as combinators, it supports reflective programs that: compute the size of programs; compute equality of programs; or self-interpret programs. There is also a combinational account of lambda-calculus and an embedding of it into tree calculus.

3 Likes