Elektrine lite

← Feed

Lane

lne@social.praxis.nyc

<p>interested in next generation type theories, braided monoidal categories, and graphical computation frameworks, based in san francisco</p>

Posts

  • View post

    From Girard. The difficulty arises from conceiving of the coherent action of connectives &amp;quot;and&amp;quot; and &amp;quot;or&amp;quot; -- but what if the problem is a matter of a lacking expressiveness by having these connectives perform double duty? It&amp;#39;s no coincidence these orderings are precisely what&amp;#39;s at stake in Yang-Baxter, which gives a pleasing geometric angle that Girard almost begins to consider: we might consider what happens when an A entangled with a B then be...

  • View post

    its pretty wild (no pun intended) that one cool trick (representability predicates) allows you to derive the pentagon and triangle coherences in untruncated hom types in higher #category-theory in #hott. its even nicer that this trick straightforwardly generalizes to monoidal categories and allows you define both levels of monoidal structure, braided structures, and even goes on to derive the hexagon coherence. all proven in cubical agda.

  • View post

    A suitable statement of my wager for so-called Virtual Graph Theory: &amp;quot;Ordinarily one first defines a category, equips it with monoidal structure, and only thereafter introduces braidings, dualities, twists, and the other phenomena of tortile geometry as additional structure. We proceed in essentially the opposite direction. We take the geometry underlying tortile structure as fundamental, and recover ordinary categorical composition and coherence as a degeneration of it.&amp;quot;

  • View post

    @MartinEscardo There is nothing magical about language here. I think that if next-token-prediction is successful it is because there is some structure inherent to the ways in which one must proceed in any given situation, which tends to be preserved in the description of scenarios narrated by various sorts of discourses; in particular the ones that make sensible the lived experiences of historic actors in various disciplines, which they rely upon when confronted by various decisions.

  • View post

    It&amp;#39;s rare to see this level of clarity from economic papers on politics, but refreshing nonetheless: &amp;quot;We consider a model of automation embedded in a political environment where workers can undertake a revolt ... we show that, starting in a democracy, capital accumulation and thus greater automation encourages the capitalists to support a coup against democracy and set up a repressive system.&amp;quot; https://www.nber.org/papers/w35336

  • View post

    When designing a program that is a dependency for other programs, one must take a lot of care in how much of the overall plan for implementation is realized before it is recommended for public use. Even if further revisions are additive, the kinds of programs that people will make utilizing a system existing at one stage of implementation will vary from what they might make using the more realized system. If your system has two phases P1 and P2: Prog(P1 + P2) != Prog(P1) + Prog(P2) in general

  • View post

    If we lived in a society that used automation to free everyone from material needs, we might be able to appreciate that having a reproducible example of a god awful/irresponsible coder/user would help us foresee the worst possible mistakes to make in systems engineering. Such could only before be discovered before at considerable expense, or when code was actually being used in live production where mistakes come at a much higher price. Claude Code ironically demonstrates this last anti-pattern

  • View post

    what if the system shell was a tool that always suffered from not knowing its semantics were best described by sequent calculus?

  • View post

    What if the core insight of Duff&amp;#39;s rc shell (Plan 9, Bell Labs), taking the sequence instead of strings as the primitive object, can be interpreted with virtual double categories as the semantic frame and sequent calculus as the type theory of its morphisms? I&amp;#39;m not entirely sure yet, but I am optimistic about what may lie in this interpretation for the shell, an often maligned setting of computation.