fwiw, one of the FFT challenges is about the Scott encoding [1], while the other uses Church trees at least [2]. Both use a balanced ternary numeral system, which is a lot more efficient than plain Church/Scott and fairly well-known [3]. Either way, I would have assumed there to be a chance that at least one of the AIs had a look at [4] -- a tutorial about FFT in LC by the benchmark creator himself.
Hover the timestamp here on HN and you'll see it at least once in your life time :) I'm guessing it's mostly developers, especially ones working internationally, who come across it every day. Others seem to prefer to convert between people's timezone, while we just send UTC+00:00 to each other.
I was about to comment that it's not UTC, it's in my local time. Then I remembered my local time (Europe/London) is currently equivalent to UTC, so I have no idea what it's actually displaying (it's not indicated in any way).
It's actually a problem in these parts that it's not obvious to us whether a time is in UTC or local time. I've found so many things displayed in UTC that people have assumed is local time then summer comes around and everything is off by an hour.
Quadtrees are also quite useful for generating fractals.
A very related project of mine, Lambda Screen [0], explores this by encoding these functional quadtrees directly in lambda calculus and rendering the structure based on Church booleans being true (white) or false (black).
With fixed point recursion, this allows for very tiny definitions of IFS fractals. For example, fractals like the Sierpinski triangle/carpet only require ~50 bit of binary lambda calculus [1] [2]!
The annihilating interaction between abstraction and application nodes is well-known in the area of interaction net research to ~correspond to β-reduction, as is also explained in the associated research paper [1].
α-conversion is not required in interaction nets. η-reduction is an additional rule not typically discussed, but see for example [2].
> α-conversion is not required in interaction nets. η-reduction is an additional rule not typically discussed, but see for example [2].
Which makes the sloppy use of "λ-Reduction" in place of "β-reduction"--the only form of reduction or conversion applied here--even less defensible. Maybe them being non-native English speakers is partly to blame?
> 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.
This is quite different. Salvadori's work aims for optimal reduction of the full lambda calculus (which requires something called "bookkeeping"/"oracle"), while HOC works on optimal/parallel reduction of a certain subset of the lambda calculus.
Both approaches have been researched for a long time now, where HOC's subset is typically referred to as "abstract algorithm". For example, a version of the lambdas calculus where any variable can be used at most once (the "affine lambda calculus"), can be reduced optimally with interaction nets without requiring any bookkeeping.
The novel thing about Salvadori's work is that it develops a new (and better explained) bookkeeping mechanism.
[1] task: https://github.com/VictorTaelin/lambench/blob/main/tsk/stre_... solution: https://github.com/VictorTaelin/lambench/blob/main/lam/stre_...
[2] task: https://github.com/VictorTaelin/lambench/blob/main/tsk/ctre_... solution: https://github.com/VictorTaelin/lambench/blob/main/lam/ctre_...
[3] https://link.springer.com/chapter/10.1007/3-540-45575-2_20
[4] https://gist.github.com/VictorTaelin/5776ede998d0039ad1cc9b1...