Pinned toot

The usual syntax for regular expressions is not a regular language because it requires parentheses. The usual syntax for context free grammars/expressions is not context-free because it uses recursion using variable names.

Is there any fundamental reason for this, i.e., some kind of diagonalization/fixed point argument or is it just a coincidence? I think the Goedelian argument doesn't apply because they are weaker than Peano arithmetic?

Eating some dogfood, probably a bit prematurely tbh (https://github.com/maxsnew/aoc-zydeco)

Surely this can't be true... #AdventOfCode as a virus scanner?

https://www.reddit.com/r/adventofcode/comments/zb98pn/2022_day_3_something_weird_with_copypasting/

According to Eilenberg and Mac Lane, they created category theory in 1945 to be able to define natural transformation, a notion that existed in the air at that time but had no definition.

But I think that the real purpose of category theory is to define the notion of universal property. Which also had traces at that time (e.g. in the desired properties of function spaces, already in 1935 in a letter of Hurewicz to Fox).

This is from the classic "Lambda: The Ultimate GOTO" paper. Sad that this is only taken seriously in functional languages to this day and we have new platforms like WASM that don't take advantage of this lesson.

Also, this is exactly how CBPV works.

1. `GOTO` is in CPBV `force`ing a thunk,

2. Pushing a return address onto the stack corresponds to the "bind" `x <- M; N` construct. You push the kont `x. N` onto the stack.

Advent of Code Day 1

We have hardly anything implemented so it ended up looking like assembly code but here's day 1 solution in our CBPV language Zydeco: https://gist.github.com/maxsnew/d0e3f47bd136aa5b3d17c906d00b38d9

Probably won't be able to keep this up very long since we haven't implemented parameterized datatypes, polymorphism or even imports yet but it was fun to get the very easy one working.

Compilers Class Musings

Close to finishing my first compilers course where I actually teach parsing/front-end in some depth. While I think there is usually over emphasis of particular algorithms over general principles, I was struck by the fact that the front-end is treated much more systematically and mathematically than the backend: different front end passes (lexing/parsing/type checking) are given mathematical specifications in terms of grammars/declarative type systems and then we need an algorithm to implement the spec.

Compare the backend where specs are usually very informal and so correctness is fuzzier. It's a bit funny bc most of my research is on semantics that only applies to the backend. But perhaps that's exactly why we emphasize mathematical specification of the front-end more: because it's already been figured out while the backend is research or at least involves more PL semantics than we can fit without a prereq.

Anyway at least this gave me the idea to give my last lecture on compiler correctness and verification and to frame it in these terms.

This is not a shitpost thank you.

A regexp is a logical formula with denotation in a set of "non standard truth values": the poset of predicates on strings rather than classical truth values {top, bot}. Empty and alternatives denote the bottom element and the join of this poset. Regular languages are closed under intersection so it is ok to add in conjunction as well. Kleene star is a particular LFP. The characters are atomic formulae and the empty string/sequencing are interpreted as a nice monoidal structure of the poset of languages (Day convolution).

A different way to say this is that regular expressions can all be interpreted as formulae in a non-symmetric variant of the logic of bunched implications where the sequencing is the *.

I haven’t done an #introduction yet, which seems to be a thing here, so:

Hi I’m Chris! I’m a prof at Northeastern (newly tenured!) researching computational tools for #gamedev, #generativeart, #storytelling, and collaborative co-creativity using PL/logic and HCI methods.

I’m neurodivergent, nonbinary, and my politics are heavily informed by Indigenous, Black, Trans and Disabled thinkers towards decolonization and anarchist interdependency.

website: https://convivial.tools

Maths and PL friends. We have PhD-student scholarships available at the University of Birmingham, UK.

In particular, Eric Finster, Vincent Rahli and myself would be very interested in getting students in type theory, homotopy theory, higher-categories, constructive mathematics, and related fields.

Please encourage your best students to apply.

https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx

Or, if you are a student reading this, consider applying:

https://www.birmingham.ac.uk/postgraduate/courses/research/computer-science/computer-science-phd.aspx

- website
- http://maxsnew.com/

- pronouns
- he/him or they/them

Real name: Max S. New

Assistant Professor in Computer Science & Engineering at University of Michigan.

PL theorist, Category practitioner

Joined Apr 2022