Linear Logic - Pond’ring Aloud

2025-03-22

Mar 22, 2025

Linear Logic and Permutation Stacks--The Forth Shall Be First

I was intrigued by the title of this paper.

Some of the statements early in that paper, though, finally set the hook. I will need to re-read this a few times.

I, also, note that this paper referenced Giroud’s Linear Logic, which is also referred to by the Ceptre paper. I was intrigued by Ceptre and think that there is some connection between it and the Nova language stuff from the Handmade Network conference talk “Democratizing Software”.

I tend to look at things from an implementation view and consider mathematical notation to be just one of the tools for manipulating these ideas. From my perspective, all of the above swirl around the same flame, along with my thoughts on PBP (Parts Based Programming, aka “0D”), FBP, etc.

Unfortunately, after 40 years of hard work, computer scientists have not been that successful at efficiently exploiting this mathematical expression metaphor. Furthermore, the single-minded pursuit of this goal has blinded us to the reason for pursuing it in the first place--to find a simple, easy-to-understand metaphor that can be used to efficiently program a variety of applications on a variety of computers.

The "standard", non-functional programming languages like Fortran, Ada, and C are the bastard progeny of the coupling between a pseudo-mathematical notation and a von Neumann-style random access memory

Perhaps it is time to move on to the next theorem.

The real Achilles' heel for these languages, however, is their innate inability to deal with parallel or distributed computation.

Summary by NotebookLM

This 1994 paper from ACM Sigarch Computer Architecture News explores the connection between linear logic, a system where resources are used exactly once, and stack-based programming, exemplified by the language Forth. The author, Henry G. Baker, argues that linear logic offers a new metaphor for programming based on the conservation of objects, contrasting it with the traditional focus on mathematical expressions and the challenges it poses for parallel computing and efficient implementation. Linear Lisp, a variant of Lisp adhering to linear logic principles, is introduced and demonstrated to have a natural mapping to a permutation stack machine, where operations primarily involve rearranging items on the stack. The paper further suggests that such a stack architecture, particularly one incorporating sophisticated permutation operations, could offer advantages in efficiency and parallelism compared to traditional register-based machines, drawing parallels to and distinctions from the design of Forth.

Further References

Lecture notes about Linear Logic

Paul’s Substack

Discussion about this post