Structural Reasoning - Zistack/program-modeling-language Wiki

All first-order relations must be considered as data. All computation must be expressed as higher-order relations.

This includes relations obtained through the composition of other relations.

Formally, this means that constraints may only be given for higher-order relations, or that only higher-order relations may be concrete. It also means that first-order relations must always be abstract. It means that no first-order relations should be constructible.


The big idea is to force all computation to be described structurally, rather than enumeratively. When computation is described enumeratively, enumeration often becomes required in order to actually analyze the possible behaviors of the program. when computation is described structurally, there is nothing to enumerate. Instead, structural equivalence (which is typically much easier to evaluate) is all that matters.

Practical Implications

No match expressions, switch/case statements, if/else statements, or anything of the sort. No lambdas, because they're too powerful and can construct the above. Encoded data cannot be manipulated without being decoded first, as there is no way to do term rewriting.

Enum values need to have some foundational primitive relations that can be applied to them in order to support computation. These primitives would say things like 'this enum's vaues are totally ordered', or 'this enum's values form a semi-lattice'.

⚠️ ** Fallback** ⚠️