So the CEO of online ads giant IAB made a pretty… remarkable speech, saying:
"These extremists (referring to privacy advocates) are political opportunists who’ve made it their mission to cripple the advertising industry and eliminate it from the American economy and culture."
And this, friends, is our mission statement RIGHT THERE.
memes liberated from work
stolen from the leanprover zulip chat: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slow.20.60positivity.60/near/322881360
The notion of model of intuitionistic propositional logic (IPL) I'm
most familiar with (being a category theory/PL nerd) is a Heyting
algebra (HA): a poset with finite meets, finite joins and a Heyting
implication. If you add propositional variables, the model includes a
choice of how to interpret them as elements of the HA and if you
include axioms, their interpretation must be true in the HA.
Then you can interpret every proposition of IPL as an element of the
HA where you interpret conjunctions as meets, disjunctions as joins
and implication as the Heyting implication. If G |- A is provable then
/\ [G] |- [A] is true.
If you look up what a model of IPL is though, you'll likely find
Kripke models, and they look at first a bit different: It's a pair of
a poset W, and a "forcing relation" ||- between elements of W and
propositions of IPL satisfying a bunch of properties:
1. for variables x, if w ||- x and v <= w then v ||- x
2. w ||- p /\ q iff w ||- p and w ||- q
3. w ||- true is true
4. w ||- p \/ q iff w ||- p or w ||- q
5. w ||- false is false
6. w ||- p => q iff for any v <= w if v ||- p then v ||- q
Despite the cosmetic difference, Kripke models are instances of the HA
model construction. Given a poset W, the HA in question is
Prop^(W^op), the poset of antitone functions from W to Prop
(classically, Prop is just the boolean order 0 <= 1). This has the
pointwise ordering: f <= g if for every w. f w implies g w.
This is a Heyting Algebra:
top w iff true
(f /\ g) w iff f w and g w
bot w iff false
(f \/ g) w iff f w or g w
(f => g) w iff for any v <= w. if f w then g w
Then an interpretation of the propositional variables in this HA would
be an assignment for each variable X and w a proposition [x] w that is
antitone in w: if [x] w and v <= w then [x] v. Then the model HA
interpretation defines exactly our Kripke forcing semantics. It
defines for each proposition of IPL p a function from W to Prop that
is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke
model is just an infix notation for this semantics:
w ||- p := [p] w
And if you unravel the definitions of the HA semantics and the HA
structure of the poset, you reproduce exactly the definition of a
Bonus: this is all a "de-categorification" of a similar situation for
lambda calculus. The Kripke models are presheaf categories and the HA
are bi-cartesian closed categories.
Working with Tusky has reminded me how great open source is if you're a programmer: If something's broken, you can just fix it. This is something you rarely notice on Android because Android itself, and all official Android apps, are a kind of pseudo-open-source where the source is available but it's real hard to build outside Google. You have to download Google's git extension tool and then clone *all of AOSP* to one app. They assume you're $GOOG internal and have access to the network drives.
Coming soon to #foot
pipe-command-output, a new "pipe terminal output to program(s) of your choice" key binding: https://codeberg.org/dnkl/foot/pulls/1237
Before this, we had pipe-visible, pipe-scrollback and pipe-selected.
pipe-command-output pipes the last command's output. For this to work, it requires shell integration; the shell needs to emit FTCS OSC sequences to signal command output start and end. See PR for details.
When I worked at #ICANN years ago there were these great pictures of early networking and Internet typologies on the wall at the main office.
You could no longer get them from the publisher, so I took pictures! Here they are in the order referred to in the final two pictures [1/2]:
what's a bird but a word
Unstoppable shitposting engine.