Lambda the Ultimate

That reminds me, from now on all comments^{(after this one)} must include a correctness proof, which will be mechanically checked by Drupal's PHP proof-checking module before it is published.

This sentence is false. :)

I appreciate the upgrade.

You know we're going to use that information to inject code into that PHP proof-checking module to make it mine Bitcoins, right?

$$\begin{array}{rcl} \mathcal{E}(T_{1}T_{2}) & \longrightarrow & \mathcal{E}'((\mathcal{E}T_{1})(\mathcal{Q}(\mathcal{E}T_{2}))) \\ \mathcal{E}'(\langle \lambda x.T_{1} \rangle T_{2}) & \longrightarrow & T_{1}[x \leftarrow T_{2}] \end{array}$$

Alas, no vau. ;-p

You know your research is esoteric when it relies on a non-standard Greek character. Lambda ought to be enough for anybody!

The MathJax TeX and LaTeX Support page summarizes what's supported. Not sure yet what the various extensions might provide. Global definitions of some common macros probably makes sense.

One should only do incremental research that fits nicely and snugly into an existing notation and formal framework. That way, you can write papers that people understand, and are easier to accept. Doing anything new will be violently rejected by the community, who really don't have the bandwidth to evaluate anything that isn't incremental given the overhead of such notation anyways.

This is why I don't play with theory very much. It is difficult to do something new because none of the existing formalisms seem to align very well.

Ya, Lambda should be enough.

One should only do incremental research that fits nicely and snugly into an existing notation and formal framework.

Ya, Lambda should be enough.

The sad thing is I see no other practical alternative. Is it true that most PL researchers can start with formalisms to understand their problems, or is it more often than not that formalisms are applied to the problem to obtain rigor after it is understood very well? If the former approach is taken, the formal framework that we start with will necessarily bias our research (what is convenient to look at in that formal framework), and in the latter case, there might not be an appropriate formal framework (that the researcher knows about and understands) for the research once the necessary understanding is achieved.

Given this problem, it makes sense to me why system researchers almost eschew formal frameworks completely (when was the last time greek appeared at SOSP or OSDI?), even though their research is quite similar to PL research in that they are both mostly focusing on abstractions.

I think you start with intuitions and fuzzy reasoning to understand your problem and resort to formalism only when you want to get it right.

If we must degenerate into seriousness:

Is it true that most PL researchers can start with formalisms to understand their problems, or is it more often than not that formalisms are applied to the problem to obtain rigor after it is understood very well?

Those are two points in an N-dimensional manifold, there are many other possibilities. People use formalisms as a guide to explore a space, and also design formalisms to fit a problem. Formalisms and formal reasoning can be useful even informally, without going so far as to prove correctness, or force you into some framework. Is there really a significant problem here?

Verily, formalism has manifold uses.

Isn't $\lambda$ like the ultimate vau or something?

Actually (at the risk of possible seriousness), haivng called the Lisp operator vau, as it's quite distinct from Lisp operator lambda, I called the rewriting-calculus operator vau because it corresponded to the Lisp operator vau. It hadn't for a moment occurred to me that the calculus would be anything like lambda calculus; and then I had the stunning realization that calculus vau is essentially isomorphic to calculus lambda, so that vau-caluclus is, more or less, an extension of lambda calculus. But I didn't rename the calculus operator, because it really does correspond to Lisp vau, not Lisp lambda. The attempt to associate Lisp lambda with calculus lambda, when they do fundamentally different things, seems to be the reason Lisp has lacked a thoroughgoing lambda-calculus-based semantics.

coincidentally, I'm working through that section of your $vau the ultimate abstraction paper right now so that I can get the semantics right for a new esoteric language (esolangs.org) .

I think it's everyone here's dream to have their research find its way into an esoteric language.

Except I didn't use that form of the letter. Conlangers may appreciate — the modern forms of the letter seemed over-similar to F, leading to possible confusion, so I chose a different ancient form of the letter that didn't survive (a left-right reflection of F), and supposed that it had undergone transformations over time analogous mutatis mutandis to what happened to the letter F.

Reading about digamma, its history of transformations seems comprehensive!

The symbol that looks like our F is (according to my hardcopy Britannica from the 1970s) the Chalcidian form of vau. I based my alternative history on the Corinthian, but I don't see that in the Wikipedia article about digamma. However, if you look at the Wikipedia artice F, the version of digamma shown there atm is the one I started from. (I ended up with something that looks pretty much like $f$, except the curve at the top goes left and the curve at the bottom goes right.)

(Aside: We're told "digamma" is called that because it looks like two gammas of different sizes written on top of each other. But as that nifty fanfic linked above notes, the ancient greeks used letters to represent numbers: alpha=1, beta=2, gamma=3, delta=4, epsilon=5, vau=6, until things got more complicated after ten. So the numerical value of vau is twice that of gamma. I've wondered about that.)

You could possibly use U+019A as a substitute. In some fonts (Gentium, for example), the 'l' is quite similar to a reversed Digamma.

edit: It actually works well in the Monospace of the comment entry box on this site, although in the Arial of the actual posts, the l is just a straight line. (Striking through an l in tex would work, but I can't find any way to do it in Mathjax.)

Hunting through unicode, closest I've come is U+285 followed by U+335, italicized, but the horizontal bar doesn't comes out quite right.

Text: ʅ̵

Mathjax: $\it ʅ̵$

[edit: somewhat better Mathjax: $\large\it ʅ\hspace{0.2em} ̵$ ]