Radix Trees — How IntMap Works

Nice talk by Tikhon Jelvis.

What FP can learn from Smalltalk by Aditya Siram

The Mundanity of Excellence: An Ethnographic Report on Stratification and Olympic Swimmers

Regular expression derivatives

United Monoids

In this blog post we will explore the consequences of postulating 0 = 1 in an algebraic structure with two binary operations (S, +, 0) and (S, â‹…, 1). Such united monoids have a few interesting properties, which are not immediately obvious

Fun with Semirings

Abstract

Describing a problem using classical linear algebra is a very well-known problem-solving technique. If your question can be formulated as a question about real or complex matrices, then the answer can often be found by standard techniques.

It’s less well-known that very similar techniques still apply where instead of real or complex numbers we have a closed semiring, which is a structure with some analogue of addition and multi-plication that need not support subtraction or division.

We define a typeclass in Haskell for describing closed semirings, and implement a few functions for manipulating matrices and polynomials over them. We then show how these functions can be used to calculate transitive closures, find shortest or longest or widest paths in a graph, analyse the data flow of imperative programs, optimally pack knapsacks, and perform discrete event simulations, all by just providing an appropriate underlying closed semiring.

More on simplices

https://bartoszmilewski.com/2018/12/11/keep-it-simplex-stupid/

Game-theoretical semantics

Game where we choose the existentially-bound variables:

forall δ. exists e. forall x. | x - x_0 | < e => | f(x) - f(x_0) | < δ

Skolem function = “my strategy in choosing values for existentially bound variables”

exists s. forall δ. forall x. | x - x_0 | < s(δ) => | f(x) - f(x_0) | < δ

Call the two players “myself” and “nature”

Definition of a game G on a sentence S:

  • (G.A) If A is atomic, then I have won G(A) and nature has lost if A is true. If A is false, nature has won and I have lost.
  • (G.&) G(S1 & S2) begins by nature’s choice of S1 or S2. The rest of the game is G(S1) or G(S2), respectively.
  • (G.v) G(S1 v S2) begins by my choice of S1 or S2. The rest of the game is G(S1) or G(S2), respectively.
  • (G.U) G((x)S(x)) begins by nature’s choice of a member of D. Let the name of the member chosen be b. The rest of the game is then G(S(b))).
  • (G.E) G((exists x)S(x)) is defined likewise except that b is chosen by myself.
  • (G.~) G(~S) is played like G(S) except that the roles of the two players(as defined by these rules) are interchanged.

The truth of a sentence S of L can be defined as the existence of a winning strategy in G(S) for myself, i.e., a way of choosing my moves such that I end up winning no matter what nature does. The falsity of S likewise means that nature has a winning strategy in G(S).

But who says that either one of us has a winning strategy? The law of excluded middle says so. On the basic game theory we now see that this law is by no means trivial or unproblematic. For in general it is not a foregone conclusion that there should exist a winning strategy for either one of the two players in a zero-sum two-person game.