Jason (jcreed) wrote,
Jason
jcreed
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
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 4 comments