You can only have one URL for each scheme though, else your compiler will report something like

error: redefinition of label 'https'

If coding is the purest form of art, then lambda calculus may be the purest form of code. Its graphical representation [1] also looks somewhat artistic.

[1] https://tromp.github.io/cl/diagrams.html

Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.

I think it's a little preposterous to conjecture that the inverse of the fine structure constant is "governed" by the expression N^2+C^2 + ((1+sqrt(5))/2)^(N-C) with N=11 and C=4. You can probably find hundreds more approximations by other arbitrary formula of similar complexity, all lacking in explanatory power of why the formula should look like that.

is the number accurate or not? and minimal aperiodic tilings of the infinite plane are not uninteresting, they are related to turing completeness. whatever. how accurate is it? you tell me.

It's far from accurate, since ((1+sqrt(5))/2)^-7 ~ 0.03444

ugh

find one. I dare you.

I just see a generic Google Drive page saying I need to request access. You may need to set public access...

correct. sorry. fixed.

I linked to the paper in a recent comment [1]. The author has been active in the Higher Order Community Discord channel for quite a while. The Higher Order Company [2] is developing HVM (Higher Order Virtual Machine), a high performance implementation of interaction nets for both CPUs and GPUs, and started the channel to discuss development and related topics, such as the Bend language for programming the HVM, discussed on HN at [3].

The paper manages to present previous work on Levy's optimal beta reduction in a more streamlined fashion, generalizing duplicators to so-called replicators that avoid the need for separate book-keeping gadgets (like croissants and brackets) . Its author also proves himself to be a skilled programmer in bringing his theory to life with this web based evaluator.

The app contrasts traditional graph-based λ-calculus reduction (which replaces nodes with entire subgraphs) with interaction (which makes only local modifications and hence needs more steps), while showing that semantics is preserved.

[1] https://news.ycombinator.com/item?id=46034355

[2] https://higherorderco.com/

[3] https://news.ycombinator.com/item?id=40390287

> there's an easy way to translate LC to IN

While easy, it sadly doesn't preserve semantics. Specifically, when you duplicate a term that ends up duplicating itself, results will diverge.

There exist more involved semantics preserving translations, using so-called croissants and brackets, or with the recent rephrased approach of [1].

[1] https://arxiv.org/abs/2505.20314

> While easy, it sadly doesn't preserve semantics.

There is actually an easy way that does preserve semantics at least to WHNF - it's called closed reduction. Mackie has worked on it a bunch (see some resources [1]).

An even simpler implementation is Sinot's token passing.

The problem with both of these approaches is the decreased amount of sharing and potential for parallelism, which is typically the reason for using interaction nets in the first place.

[1] https://github.com/marvinborner/interaction-net-resources?ta...