Readings & Marginalia

The main interest of AUFBAU, much like it's inspiration and subset implementation Outlines is generality. As Mündler and his colleagues demonstrated it in their paper, writting constraint gen for a particular language is not that hard, though probably a bit tedious.

The end goal, in our view is to have a strong enough implementation so that we can declare proof-checkers in the aufbau grammar spec. This would be huge. First it would allow us to have constraint proof-search, but in it of itselft, it is also a very powerful semantic statement.

However, we lack a truly general definition of what a constraint is, and since most of our semantic constraints are typing constraint, what is a type ? Every formal system will have its answer, and we could go implementing them one by one, with reduction rules, and all the machinery, but it doesnt feel right.

Our first version used a sort of compormise, where a type language live in parralel with the EBNF defined grammar, but they can unify when needed with pattern matching and sort of substitution rules.

It works, but it's not very satisfying, and this is why we are currently working on new definitions.

The most generalizable definition

First, a type posseses some sort of relation to syntactic elements. It has an input string representation, that might be reducible and non-canonical but that is equivalent to its canonical form. Thanks to the CG-grammar, the parser can trasnform any input string into a syntactic tree.

Is is over this tree form that type chekcing operates, with three atomic operations:

• Shape unification: \(A \to B \equiv \top \to B \equiv A \to ( B )\)
• Ascription: \(x: \tau\)
• Normalization: \((A \to B)A \implies A\)

Shape unfication is generalized and corresponds to hole resolution + the application of some elaboration rules Ascription is just a constraint propagation mecanisms Normalization works with grammar specific normalization rules

TODO

This is a first step towards fully general stuff. Normalizaiton needq a lot of expansion to be abe to support complex type systems. byt the skeleton is good.

In 6.54 of the Tractatus Wittgenstein writes:

My propositions are elucidatory in this way: he who understands
me finally recognizes them as senseless, when he has climbed out
through them, on them, over them. (He must so to speak throw
away the ladder, after he has climbed up on it.)

This strangely relates to the process of building a formal system. We always have to work with a language that is different from the one we want to talk about. We always have to use a more permissive language as the constructor of the system, and use concepts that have, by all accounts no meaning that interests us the the system we are building. I think this is echoed by model theory, and incompletness theorems, but this aspects deserves more thought.

We always have to use a ladder. Natural language is the most powerful ladder, and we can describe any system in it. In other words, every logical construct relies on a part of mystical in it's justification (in the sense of 6.522). This mustn't be considered a fatality, but rahter kept in mind as part of the process. This approach is core to [USI's formal systems work]{AUF-02}.