expressivity

[gusl]

hmm... proof theory... (imagine a lip-licking emoticon, or a Homer Simpson voice)

from Around Gödel's Theorem - Ch 6.4: On the size of proofs

...
Theorem on the Size of Proofs.If T is a fundamental formal theory, and a closed formula H is not provable in T, then for each computable function f(x), which grows to infinity, there is a theorem K of T such that

|K|_T+H < f(|K|_T). [ |K|_T+H means "the size of the proof of K in theory T+H" ]

For example, let use take f(x) = x/100. There is a theorem K1 of the theory T such that its proof in the extended theory T+H is at least 100 times shorter than its shortest proof in T. You can take also f(x) = x/1000, or sqrt(x), or log10(x) etc.
...

I wonder if this is relevant to the broader concept of expressibility.

Obviously there can't be a (shortest proof <~> shortest program)-analogous result: since all good languages are Turing-equivalent, then for all problems, its Kolmogorov Complexities are bounded by a constant of each other (the size of the interpreter for the language into a standard computing machine).

When thinking of Logic and Computation side by side, I always think of this difference: logics have limited expressivity, whereas computational systems always have maximum expressivity.

So when we talk about "expressivity" in the context of programming languages, we mean something else entirely: how easy and natural is it to express what we want? Maybe we should use a new word, like "expressibility".

The literature on this subject seems to be very poor: Felleisen being the only reference I could find, besides fare of course. I think this warrants a philosophical essay at the very least, in order to properly define "expressivity/expressibility" and discuss possible measures.

Comments

[gustavolacerda.livejournal.com]

That's lovely! It's exactly the kind of "fundamental constraints" result that I find so nice... which is probably the main reason I like KC in the first place.

[mathemajician.livejournal.com]

Yeah, KC things are cute. The problem is that every time you're doing something and you think that you have a result that looks really interesting you naturally start to think it could be useful for something... and then you remember how horribly impossible it is to compute or even estimate.