Jason (jcreed) wrote,

Made a ton of good progress thinking about this differential privacy type system. Sorted out a bunch of previously confusing issues with what the context means, with fixpoints, with recursive types, and with function types. Abandoned the notion that there are special metric vs. non-metric types. Category theory meditation revealed what the monoidal-closed function space (i.e. lollipop) has to be: the distance between two functions is their l1 norm, i.e. the distance between them pointwise in the worst case. Decided to think about the metric in terms of a judgment (v1 ~x v2 "these two values are at most x far apart") rather than functionally (d(v1,v2) as "the distance between the two values"), since function types' metric being defined so extensionally makes it undecidable anyway.

The hilarious thing to me personally is that this whole line of work is fundamentally a fleshed-out version of a section from my SIGBOVIK '09 "Choose Your Own Logic Adventure", except adapted to affine logic rather than linear logic.

Watched the first episode of "It's Always Sunny in Philadelphia", since my sisters gave it to me as an early xmas gift. Pretty funny. It nearly hit my "oh god this is so awkward I just have to stop watching" button several times but moved on quickly enough in each case.
Tags: television, work

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded