Benton’s Linear/Nonlinear
Logic has
models in (lax) monoidal adjunctions between monoidal and cartesian
categories.
The tasks performed in GPU kernels often deal with linear and
nonlinear maps between real vector spaces.
I want to take this and run with it: let’s see what it looks like to
define some mixed linear/nonlinear functions in a linear/nonlinear
type theory. This feels to me so obvious that it must be written down
somewhere already. In the literature there is work that gets close
(and I’ll do some comparisons at the end), but none are quite what I
want. Please let me know if I’ve missed something.
For a little while I have been working on this port of Kenzo from
Common Lisp to Haskell. Kenzo is a collection of algorithms for
explicit constructions on simplicial sets: the
README in the
repository gives a list of what’s implemented and what should be
possible. The algorithms and implementations in Kenzo were created by
Francis Sergeraert, Julio Rubio Garcia, Xavier Dousson, Ana Romero and
many collaborators.
My goal was to implement just enough to compute \pi_4 S^3,
and I reached it today.
...
> let x = totalSpace s3 (Wbar kz1) fibration
> putStrLn $ "π₄ S³ is: " ++ show (homology x !! 4)
π₄ S³ is: ℤ/2
A fun capability it picked up along the way is calculating the
homology of Eilenberg-MacLane spaces K(ℤ/m,n), for example, here is
K(ℤ/3,2).This makes my laptop get hot pretty quickly.
I have a lot of ideas for improvements and additional features if
anybody is interested in joining in, so please email me if that’s
you or you know a student for whom this would make a good project.
For example, adding the construction of loop spaces and their homology
would be nice, as would homotopy pushouts in general.
On the implementation side, I have not spent any time optimising the
code and there are some obvious places to start, like using a proper
integer matrix library instead of a homemade one. These sorts of
optimisations would also make a good project for an undergraduate,
with not much mathematical background required.
Below, I’ve copy-pasted a quick introduction I wrote to the ideas
behind Kenzo.
