Unlimited register machines

Stream: CSLib

[Jesse Alama]

I've been working for a few weeks on adding URMs (unlimited register machines), and would like to announce my work. I've just opened a PR.

URMs are a machine model of computation that's a bit closer to what we'd recognize as a "computer" than a Turing machine, in that it has a notion of instructions (and programs) and registers. One imagines a machine with an infinite sequence of registers, each containing a natural number (unbounded). One computes by evaluating programs, which are sequences of four instructions:

• Z n — set the content of register n to zero
• S n — increment the content of register n
• T m n — copy the content of register m to register n
• J m n q — if registers m and n are equal, jump to instruction q; otherwise, continue to the next instruction

The PR includes the basic instruction type, program representation, execution semantics, and foundational lemmas about straight-line programs and halting behavior.

While Mathlib has some Turing machine content, URMs feel like a natural fit for CSLib given its focus on algorithmic computation models. My longer-term goal is to prove the equivalence of URM-computability with CSLib's existing SKI calculus, establishing another bridge between computation models in the library. I actually have a proof of this result ready to go but am more interested in getting your feedback on the basics before asking for review on a large PR. I also see URMs as a nice base layer on which to build other languages and machine models, leveraging Lean's macro system. URM could also be a nice source of examples for exercising grind, especially when it comes to verification of concrete (URM) programs.

I'd welcome feedback on the API design, naming conventions, and overall structure. Are there aspects of URM theory that would be especially valuable to prioritize?

[Shreyas Srinivas]

@Jesse Alama : I am trying to write a more universal model in cslib#275

[Shreyas Srinivas]

It could subsume this model as a query

[Jakub Nowak]

You still need to write the model as a query, which is homologous to the work Jesse did...

[Shreyas Srinivas]

Yeah, but it could be fitted into this framework

[Shreyas Srinivas]

Then you get to easily write reductions from this model to other models and vice versa

[Jesse Alama]

It looks like the query model is tailored to time complexity analysis, whereas the URM approach -- at least how I've sketched it -- is more about computability. It seems there's room for both approaches! I'd be happy to help work out how to embed URMs to the query model.

[Jakub Nowak]

Hm, to prove that something is computable is it not enough to write Lean code that computes it? (and you can prove, that it is correct in Lean)

[Jakub Nowak]

At least it proves that it is computable in the computational model that is Lean I think? But we don't have formal proof that Lean computation model is equivalent to TM.

[Jesse Alama]

@Jakub Nowak I share your concerns! The gap between "computable in Lean" and "computable in a formal sense" is exactly what motivates this kind of work.

Two relevant pending results that help bridge this:

1. I have a proof of the equivalence of CSLib's SKI calculus with Turing machines (TM0), which would establish that connection within CSLib.

2. For Mathlib, I also have a proof of TM → Partrec (every function computed by a Turing machine is partial recursive). Mathlib currently only has the reverse direction (Partrec → TM, in TMToPartrec.lean), so this would complete that equivalence.

Together these would give a chain: SKI ↔ TM ↔ Partrec, formally connecting different models of computation.

[Jakub Nowak]

I'm working on similar thing, but for call-by-value lamdba calculus, i.e. proving call-by-value lamdba calculus is equivalent to turing machine as computational models. With your work, I can choose to prove the equivalence with SKI or Partrec (or URM, if you plan to do that too), instead of TM, which might be easier. I'm looking forward to also seeing your approach for these proofs.

[Shreyas Srinivas]

Jesse Alama said:

Jakub Nowak I share your concerns! The gap between "computable in Lean" and "computable in a formal sense" is exactly what motivates this kind of work.

Two relevant pending results that help bridge this:

1. I have a proof of the equivalence of CSLib's SKI calculus with Turing machines (TM0), which would establish that connection within CSLib.

2. For Mathlib, I also have a proof of TM → Partrec (every function computed by a Turing machine is partial recursive). Mathlib currently only has the reverse direction (Partrec → TM, in TMToPartrec.lean), so this would complete that equivalence.

Together these would give a chain: SKI ↔ TM ↔ Partrec, formally connecting different models of computation.

Sounds good. Glad to be of help. I am a bit busy for the rest of this week. But hopefully the examples already uploaded in the PR are helpful

[Shreyas Srinivas]

I actually just posted a challenge to put TMs inside this model here : #CSLib > Query model for Algorithms complexity : updates @ 💬

[Chris Henson]

Shreyas Srinivas said:

Jesse Alama : I am trying to write a more universal model in cslib#275

It could subsume this model as a query

@Shreyas Srinivas I don't think we want to have your proposed query model attempt to encompass every single development related to complexity theory. After that PR is cleaned up and merged, you could certainly try some proofs of equivalence to other parts of the library, but my viewpoint is that we do not want every single development in CSLib to be through this monadic framework, as there are tradeoffs with more standard deep embeddings.

[Shreyas Srinivas]

That’s fair but one of my goals with the query model is to make it trivial to lift algorithms between models more systematically

[Shreyas Srinivas]

This is needed for example when doing circuit complexity upper bounds. Typically you need a bounded time complexity computation (say on a model of TMs) that produces a circuit and then you need the circuit to compute things.

[Shreyas Srinivas]

More concretely I agree that deep embeddings have benefits. But I think a shallow embedding can co exist and be useful as well.

[Chris Henson]

Jesse Alama said:

Together these would give a chain: SKI ↔ TM ↔ Partrec, formally connecting different models of computation.

@Jesse Alama I look forward to these future PRs as well! I am excited to see some connections to other parts of CSLib via SKI.

For this PR, I will try to start reviewing sometime in the next week or so.

[Alex Meiburg]

Question about this URM model: is there no notion of "dereference a register"? Otherwise this seems like a program can only manipulate a finite number of registers ever.

[Jakub Nowak]

Alex Meiburg said:

Question about this URM model: is there no notion of "dereference a register"? Otherwise this seems like a program can only manipulate a finite number of registers ever.

You only need 2 registers to be Turing Complete. At least for the Minsky Machine, not sure about URM, but I'm guessing you also only need 2 or 3. https://en.wikipedia.org/wiki/Counter_machine

[Snir Broshi]

btw there's a great Computerphile video that proves 2 registers are sufficient to be Turing complete:
https://www.youtube.com/watch?v=PXN7jTNGQIw

[Ching-Tsun Chou]

Just curious: Would URM be easier to use if the program is a graph modeling a flowchart, rather than a list of instructions?

[Alex Meiburg]

Ah, okay. I was familiar with the fact that 2 suffices for Turing completeness, I thought this was a "model" in the sense of, say, "the Real RAM model", for writing down programs and so on.

[Alex Meiburg]

I get it now. :) Cool!

[Thomas Waring]

Jesse Alama said:

My longer-term goal is to prove the equivalence of URM-computability with CSLib's existing SKI calculus, establishing another bridge between computation models in the library.

Very glad to see that the SKI developments are proving useful! I had grand plans of proving Partrec -> SKI (most of the pieces ought to be in SKI/Recursion) but never got around to fixing what it means for a term to compute a partial function in a way I was 100% happy with. If there are any developments on the SKI side that would be helpful please let me know :-))

[Thomas Waring]

More generally it has seemed to me for a while that we need a formal notion of "computability class" or something of the sort, or at least a way to say that two notions of computation are equivalent in strength in a non-ad-hoc way — though tbf we would then need to fix what a "model of computation" is, &c&c

[Chris Henson]

@Fabrizio Montesi I think your comments on cslib#299 have been addressed, I've set it to merge once you approve. (Just pinging here since the PR has gotten a bit noisy)

[Fabrizio Montesi]

Thanks, I'll have another look asap. :⁠-⁠)