With a little engineering rigor we could do a push-down automata with semantics Girards-Reynolds constrained around polymorphism.
Utilizing Girard-Reynolds constraints on a polymorphic push-down automata fundamentally misconstrues both computational topology and dynamic system semantics..
The ability to checkpoint the precise state of an agent interaction, bound it above by that context, evaluate within the context is trivially useful. It’s a bit of poetic license maybe to call that a push down automata. What I mean by the analogy is that systems ranging from BERTopic to the Humanify JS de-minifier employ large, positive-temp LLM-style models in bounded ways, for better outcomes, in conjunction with deterministic techniques. In fact, in the case of Humanify, push-down automata are trivially involved via the PLT in the conventional de-compilation.
Girard-Reynolds is again a bit of an analogy though not without plausible concrete application: even post-softmax in a GPT there are useful types one can imagine as being amenable to parametric polymorphism and therefore dictating their implementations.
If your comment is roughly: “that’s not literally sound as stated”, point conceded, it’s a one-sentence allusion to real rigor, not real rigor itself.
Do you find any of that controversial?