Notebook

Introduction

This ever-expanding document started as a set of study notes and exercises and gradually outgrew itself to become more encyclopedic. Having all these notes in one place is quite helpful for both expressing my own thoughts clearly and for later reference. It is also helpful for tracking connections between seemingly unrelated concepts --- the entire monograph is hyperlinked. Even though I aim at understanding every concept in the way it is meant to be used, most concepts are presented insomuch as they are relevant to my previous experience.

Since these are study notes, they will naturally have a lot of errors, so read them with caution. The document claims no referential nor pedagogical value. Everything is written at the level of abstraction I am comfortable with. Furthermore, some sections in the monograph are much more polished than others. Feel free to contact me if something in this monograph happens to distress you.

I tried putting citations on as many things as possible. The citations themselves are usually put in the left margin. If there is no citation on a definition or theorem, that means that I have either recalled it from memory or discovered it on my own. I try to mark my own definitions to distinguish them from one taken from other sources. Many of the unoriginal definitions and theorems are restated. The simple proofs are mostly original, and the difficult ones are, often loosely, based on proofs from the places cited. Some proofs simply state "Trivial." in order to distinguish themselves from the proofs that are omitted for other reasons.

Last but not least, some auxiliary programs are provided in the code/ subdirectory within the monograph's source. Staying close to the monograph exposition is a priority over performance or code quality considerations.

License

This is a public domain project: it uses CC0 for the text itself and the Unlicense for the Python code.

Project structure

While I have put in a lot of effort into the project structure itself, I believe that, because of the nature of the project, it makes little sense to document it extensively. There is a GNU Make file specifying how to build the document. There are also several custom tools that can be found in the code/commands subdirectory - they are most easily activated via poe (poe --root code <command>).

If you happen to be interested in any aspect of the setup, feel free to contact me.

Build system

There are two build systems --- the makefile and the code.commands.watcher (Usage: poe --root code watcher [--no-aux]) command. The first one is aimed at full builds, i.e. for continuous integration, while the second one is aimed at incremental builds, i.e. for development.

There are externalized figures in the figures directory of the following kinds:

• Asymptote (.asy) files for 2D and 3D sketches and plots.
• tikz (.tex with document class classes/tikz or classes/graphs) files for graphs.
• tikz-cd (.tex with document class classes/tikzcd) files for commutative and Hasse diagrams.
• forest (.tex with document class classes/forest) files for trees.

Parsers

A lot of the monograph-related code, as well as some of the tools are based on a recursive descent parser framework created specifically for various (micro)languages in the monograph:

• Natural deduction rules
• Formal grammar schemas
• First-order logic terms and formulas
• Untyped lambda calculus terms
• Plain text

Two additional parsers are included:

• (Limited) LaTeX
• (Opinionated) BibTeX

LaTeX tools

There is a tool, code.commands.format_matrices (Usage: poe --root code format-matrices figures/*.tex), made specifically for formatting LaTeX arrays and similar environments.

Bib(La)TeX tools

There is a set of tools, code.commands.bibtools (Usage: poe --root code bibtools), consisting of:

• A formatter (... format bibliography bibliography/*.bib)
• Several BibLaTeX entry fetch tools:
  • ... fetch doi <id>
  • ... fetch isbn <id>
  • ... fetch arxiv <id>.

Some comments should be made about the parser. It was created specifically for maintaining my personal (digital) library and this monograph's sources in particular.

• The parser only allows the fields from the BibEntry class. Because this tool was built upon years of maintaining references with other improvised tools, however, a lot of (standard and nonstandard) entry properties accumulated.
• The parser auxiliary logic for handling author names via the BibAuthor class. This involves parsing and handling each author separately (with and acting as a separator). Names are assumed to be in the format Last, Title, Other, Title and Other being optional and Other containing first and middle names. For Cyrillic languages, Latin transliteration is enforced via the BibAuthor.display_name field that gets read and written to the shortauthor BibTeX field.
• The parser tries to unescape certain characters like & and @, while BibEntry tries to escape them when serializing. Exceptions for this are the fields marked as "verbatim" such as url.
• The parser also supports verbatim fields, i.e. fields with values enclosed in an additional pair of curly braces like {{value}} or "{value}". The value inside does not get processed by the author processing mechanism, thus we can treat "corporate names" like {{Springer Science and Business Media}} as one.