#expressibility

[kratowords]

By studying a number of examples, we have come to the conclusion that programs in less expressive languages exhibit repeated occurrences of programming patterns, and that this pattern-oriented style is detrimental to the programming process.

Felleisen, "On the expressive power of programming languages"

[kratowords]

_The C-only train has left the station_. Few departments teach surveys of programming languages anymore, and I don’t know of any department that teaches a required course in history of computing. I worry about what this means for our discipline. Are we really going to tell students that **the peak of human expressibility for computation was in 1973**? That all programming language research from here on out is wasted energy? That simplicity is all that we can ever hope for, and correctness and consistency just aren’t worth working on? Are we forever stuck with 30+ year old ideas and don’t even teach that anything else is possible?

https://computinged.wordpress.com/2009/08/14/lisp-and-smalltalk-are-dead-its-c-all-the-way-down/

[word-association]

Things you provably can't do in first-order logic

Express connectivity in a graph, that sort of thing. 

"Why graphs?"

Graphs are cool. The railway network from here? That's totally a graph:

And you can represent graphs in first-order logic. All you need are individual constants for the vertices and a binary relation \(\mathsf{E}(x,y)\) for the edges. 

\[\ast\ast\ast\]

\[\exists x \forall y \mathsf{E}(x,y)\]

Or that any two different vertices have an edge going from one to the other:

\[\forall x \forall y (x \neq y \rightarrow \mathsf{E}(x, y))\]

Or that any vertex is connected to exactly one vertex:

\[\forall x \exists y (\mathsf{E}(x,y) \wedge \forall z (\mathsf{E}(x, z) \rightarrow y = z))\]

Or that there's a path of length 2 connecting any two vertices:

\[\forall x \forall y \exists z_1 (\mathsf{E}(x, z_1) \wedge \mathsf{E}(z_1, y) \wedge x \neq z_1 \wedge y \neq z_1\]

What you're basically trying to capture here is this situation:

Other properties, like connectivity, you can't express.

\[\ast\ast\ast\]

"What's connectivity?"

Connectivity is when between any two nodes of a graph there's a path of some finite length \(k \in \mathbb{N}\).

"Like, an edge?"

That's one possibility, when \(x\) and \(y\) are directly connected by edge. But you can also have an edge going out from \(x\) to something that has an edge going to something that has an edge etc., all the way to \(y\).

\[\ast\ast\ast\]

"Why can't you express that?"

Suppose you can. Suppose there's a first order formula \(\phi\) that expresses connectivity for a graph.

Now take two new constants \(a\) and \(b\) and consider the following formulas:

\[\psi_1 = \lnot \exists z_1 (\mathsf{E}(a, z_1) \wedge \mathsf{E}(z_1, b) \wedge a \neq z_1 \wedge b \neq z_1)\]

\[\psi_2 = \lnot \exists z_1 \exists z_2 (\mathsf{E}(a, z_1) \wedge \mathsf{E}(z_1, z_2) \wedge \mathsf{E}(z_2, b) \wedge \bigwedge (a \neq z_i \wedge b \neq z_i \wedge z_i \neq z_j))\]

\[\dots\]

\[\psi_n = \lnot \exists z_1 \dots \exists z_n (\mathsf{E}(a, z_1) \wedge \dots \wedge \mathsf{E}(z_n, b) \wedge \bigwedge (a \neq z_i \wedge b \neq z_i \wedge z_i \neq z_j))\]

\(\psi_1\) says that there is no path of length 2 from \(a\) to \(b\). \(\psi_2\) says that there is no path of length 3 from \(a\) to \(b\), and so on. \(\psi_n\) says that there is no path of length \(n+1\) from \(a\) to \(b\). There's an infinite number of \(\psi_i\)'s, one for each \(n \in \mathbb{N}\).

Now we can do business. Take the following sets of sentences:

\[\mathcal{A} = \{\psi_i \mid i \in \mathbb{N}\}\]

\[\mathcal{B} = \{ \lnot \mathsf{E}(a, b), a \neq b\}\]

\[\mathcal{C} = \{ \phi\}\]

The claim is that \(\mathcal{A} \cup \mathcal{B} \cup \mathcal{C}\) has a model. But this is bad, because in this model we have that any two nodes are connected (because \(\phi\) is true in it), which means that there's a path of finite length between them. However, when you consider \(a\) and \(b\) you realize that there can be no finite path between them. Because of all the \(\psi_i\)'s and \(\mathcal{B}\) there isn't a path of length 1, or 2, or 3, or any finite number. So the assumption that \(\phi\) expresses connectivity leads to a contradiction.

\[\ast\ast\ast\]

"Why does \(\mathcal{A} \cup \mathcal{B} \cup \mathcal{C}\) have a model?"

Because of the Compactness theorem.

"What's that about?

It says that a set of first-order formulas has a model iff each of its finite subsets has a model.

"That's really a thing?"

Yeah, it's how you usually show that infinite sets of sentences have models.

\[\ast\ast\ast\]

"So how do you know that every finite subset of \(\mathcal{A} \cup \mathcal{B} \cup \mathcal{C}\) has a model?"

Ah, well let's see.

Most of the combinations are easy. For instance, each of \(\mathsf{B}\), \(\mathsf{C}\) and \(\mathsf{B} \cup \mathsf{C}\) has a model, for instance this works for all of them:

The interesting case is \(\mathcal{B}\) plus \(\mathcal{C}\) plus a finite subset \(\mathcal{A}^\prime\) of \(\mathcal{A}\). In this case take the largest index \(n\) in \(\mathcal{A}^\prime\) and define a model where there's only a path of length \(n+2\) from \(a\) to \(b\):

You can see that this graph is connected (i.e. \(\phi\) is true), and each of the \(\psi_i\)'s in \(\mathcal{A}^\prime\) is true, because there is no path of length \(n+1\) or smaller between \(a\) and \(b\).

\[\ast\ast\ast\]

This is cool, no?

"What? Sorry, I dozed off."

[webtrovert]

YOU NEED TO STOP

you think you can hide on your personal.

no qurl

i see you

i see me too

WE NEED TO S T O P AND SMELL THE F A I L U R E IF WE KEEP DOING THIS

[planetracks]

expressibility replied to your link: there are so many blogs on my favs. oops. but follow them all

zomg sarah why did you put me there i’m not a black and white blog XD <3

because you're my favourite and your personal is better than andrews. <3