Integrating Diverse Aspects of our Researches

Chris

Constructor theory, https://www.constructortheory.org/, is a relatively new view of physics and computation led by one of the foundational voices in quantum computing, David Deutsch. It posits a substrate of data containing constructors, which are capable of computational tasks, including the creation of new constructors. This is different from a Turing Machine in that the computing head is actually data and can recreate itself where a Turing Machine cannot. This view of computation where code is data will be familiar with programmers of Lisp and other declarative languages.

At the same time, Constructor Theorists are occupied with factuals and counterfactuals rather than formulas that express physical laws. These being discrete statements about what is or is not possible in a system, the resulting models from this approach would be state machines rather than flow models, justifying our original emphasis on finite state machines in our researches.

The utility of FSMs in designs of both physical and virtual machines is further borne out by the researches of Leslie Lamport, known for the Lamport Clock, Paxos, and the Bakery Algorithm. All that is lacking is a language to describe our state machines.

Lambda Calculus and Category Theory are our languages for describing our physical and virtual machines respectively. The axioms of the lambda can be combined to form the same logic elements as transistors can, but lambda calculus is unwieldy for large models. For these, we need a language that maps other mathematical and physical constructs to the lambda, which describes Category Theory.

Combining these elements, we have the basic tools for mapping the boxes and arrows of an FSM design into gates that can be engraved on silicon as well as higher level abstractions that can be humanly manipulated. While this mapping isn’t trivial, it is provable and it is a sound basis for design. Category Theory is known for arrows and monads. Oversimplified, arrows are functions and monads are boxes.

Propagators, truth maintenance systems and domain specific languages are three of many high level constructs that are supported more cleanly by programming paradigms descended from lambda calculus and Category Theory than those pragmatically following from the silicon. By clean support, I mean that an expert in an application area can learn at least one technique for expressing their knowledge in a computationally accessible way.

Type Theory is a better way to order computation than rote transcription of formulas. For a trivial example, “d = rt” is supposed to give us distance when rate and time are supplied, but that formula assumes that the units are compatible. Type Theory says that a rate in km/h and a time in hours will give us a distance in km, because km is of type distance and you should multiply km/h by h to derive km. The difference between type theory and formulas is that you can do algebra with types (as shown), and therefore types are computable; rote formulas are “give a man a fish” where Type Theory is a whole fishing academy.

This was easier and more succinct than I expected, so doubtless there will be omissions and also questions left unanswered. Please help me by letting me know where it would be helpful to unpack this dense prose and make more explicit connections and where you’d like references.

theruran

Chris I’ve been learning more math lately, and it is definitely helping! I understand a few basics of category theory, like what is a functor. Here is what I can tell about a kind of bootstrap or hierarchy for computing:

Proof theory: e.g. Nested Sequent Calculi, and/or Symmetric Interaction Combinators, which can be used as an execution model of lambda calculus. See HVM2 white paper
Computation: lambda theory in general, John Shutt’s vau calculus in particular. Vau calculi need to be studied more - the main difference is that the language semantics allows you choose when to evaluate an expression, thus eliminating the need for an ill-specified macro language such as Scheme’s. See: “Fexprs as the basis of Lisp function application or $vau: the ultimate abstraction” by John Shutt, PhD thesis (2010)
Computational logic: Now that we have proof-theoretic computation, we can bootstrap theorem provers AKA proof assistants. For one, we need a subset of first-order logic to automatically prove theorems in Conjunctive Normal Form with an SMT solver. Intuitionistic Modal Logic has been used for software and hardware formal verification, since it allows unary operators that encode the certainty of a proposition. See: Propositions-as-Types, Doxastic logic, Epistemic modal logic, Description Logic, “Nested Sequents for Intuitionistic Modal Logics via Structural Refinement” by Tim S. Lyon (2021)
Computational type theory: With proof-theoretic computation and first-order logic theorem prover(s) in place, next bootstrap the strongest type theory available, such as Unified Theory of dependent Types (UTT) by Zhaohui Luo, an extension of Martin-Lof Type Theory (MLTT), or the more modern Cartesian Cubical Type Theory. See:
- “Abstract and Concrete Type Theories” by Taichi Uemura, PhD thesis (2024)
- “MTT-Semantics is Model-Theoretic As Well As Proof-Theoretic” by Zhaohui Luo (2019)
- “A unifying theory of dependent types: the schematic approach” by Zhaohui Luo (2005) doi:10.1007/bfb0023883
- “Programming in Martin-Lof’s Type Theory: An Introduction” by Nordstrom, Petersson, Smith (1990)
- “An Extended Calculus of Constructions” by Zhaohui Luo, PhD Thesis (1990)
- “Towards a practical programming language based on dependent type theory” by Ulf Norell, PhD thesis (2007)
Category theory: Now we can build a formally-verified library of category theory for reasoning about stateful programs, and other software and hardware constructions - in particular, we need monads for modeling effects and input/output.
Abstract State Machines: (ASMs) There is a whole systems engineering methodology here for creating a ground model that represents requirements on the system-of-interest, then through successive refinement, we can build FSMs in the abstract space then extract the proofs to data formats for hardware detailed design specifications. ASMs cleanly model databases which are of central importance in computing that isn’t full of fuck.
??? many things are possible with these strong theoretic foundations. Cryptographic systems will be critical to build next, and will make strong use of the many theories listed above so they may proven correct-by-construction.

theruran

Here Philip Wadler asked, are there any more? Because he argues that the Curry-Howard correspondence was discovered rather than invented. Logicians on the left, computer scientists on the right. How does this extend to computer hardware?

stman

When you talk about a proof assistant, and with the goal in mind of the universal engine to get rid of complex compilers, do you mean that we shall provision parallel computation means for a live proofer in the universal engine ? The universal engine is currently a two level pipeline processing engine :

Level 1 : Pseudo-code instructions level, that are a very complex instructions set, as they handle natively most of high level languages.
Level 2 : Each pseudo-code instruction is coded into a microcode assembler, designed to play fast and easily with all the many registers available easily, but also perform raw access to memory and IOs. Such microcode programs come with the help of tiny FPGA allowing to implement hardcoded logic to speed up or make some pseudo-code instructions coding in microcode easier.

So the question is : Where to provision what would be necessary to handle a proofer here ? And what would that actually mean ? Is it possible or are we asking the impossible ?

Chris

SKI Combinator Calculus is a possible ISA for our machine. Taken in reverse, I(a) => a, K(ab) => a, and S(abc) => ac(bc), where a, b, and c are binary trees. A binary tree of the AST of any program can be assembled such that branches always terminate with S, K, or I as the leaf. That ‘I’ could be replaced by SKa for any a, including S or K, and is therefore syntactic sugar, hints that any combinator which can be conveniently mapped to silicon might similarly be added to the ISA, e.g. numbers can be encoded in binary rather than Church numerals where such would be useful and Boolean operations like ‘and’, ‘or’, or ‘not’ can be represented with conventional gates

This represents an enormous amount of work and I have no idea whether it’s possible to configure an FPGA to apply the S combinator or, exactly, how this works in the context of the previous discussion about register machines. My intuition suggests that it’s possible, so I’m putting it out there for the minds of my comrades with a more rigorous bent to vet the idea

Also, what type of FPGAs are we looking at? Maybe trying to implement the S combinator and application on a specific target would be the way to eliminate or justify this intuition

stman

Chris You mean forthe second stage processing unit, the one called microcode processing unit ? Or are you refering to the pseudo-code processing unit ?

Chris

Combinators as microcode. K, I, and many other combinators have concrete TTL implementations. The S combinator is a little esoteric and I have yet to take the time to see if a TTL implementation is possible

theruran

Chris Combinators as microcode.

I love it!

vidak

beep just logged in again, will read this thread soon.

vidak

i think i have somewhat of a grasp of the theory.

i think much of my contribution will be taking this theory chris has elucidated and try and realise it in practice.

i have some understanding of how to microcode a CPU, i have some suggestions about maybe using a stack machine architecture, in order to realise the thing in silicon.