LtU now supports Mathjax

LtU now supports MathJax, which allows the use of TeX markup in posts and comments. Note that only TeX/LaTeX markup is currently supported - the alternate MathML format conflict's with the blog's HTML sanitization.

This enhancement is dedicated to neelk, who most recently suggested this feature just over a year ago.

When I went searching for a bit of Mathjax-compatible LaTeX that was relevant to programming languages, the first good example Google found for me was on Neel's blog:

\newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}
\newcommand{\letv}[3]{\mathsf{let}\;{#1} = {#2}\;\mathsf{in}\;{#3}}
\rule{\judge{\Gamma}{e}{T(A)} \qquad
\judge{\Gamma, x:A}{e'}{T(C)}}

Copy-pasting the above and making it work immediately made it clear that we're going to need a package of useful macros. But it's a start. Feedback welcome.

Note that MathJax rendering is entirely client-side - if you don't see a well-formatted formula above, check the MathJax browser compatibility page and their FAQ.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

As if we weren't too

As if we weren't too highbrow already... Thanks, Anton!!

That reminds me

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.

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?


\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}]

Alas, no vau. ;-p

Abandon lambda at your own risk

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

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.

Sense and sensibility

One should only do incremental research that fits nicely and snugly into an existing notation and formal framework.
Glad to see someone making sense around here. After Turing completeness, everything else is just subjective niceties designed to impress program committees and web developers. A little tar never hurt anyone!
Ya, Lambda should be enough.
It's not like anyone's going to be doing any useful work outside of a cartesian closed category anyway.

The sad thing is I see no

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.

Excluded middle

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.

Perhaps I should just add vau to MathJax

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?

My LaTeX code for vau transforms \(f\) using pstricks

Verily, formalism has manifold uses.

Isn't \(\lambda\) like the

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

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 ( .

Congrats John

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

Cool beans

\(f \sqsubset \lambda x. x \bot \)

(And thank you, Anton)

Nice but not strictly necessary

\(f \sqsubset ϝ x. x \bot \)

I cut and pasted a proper Unicode vau there instead of \lambda, and all is well, except that the font makes it look too F-ish for my taste. (ϝ is the ancestor of F, as we learn from "For Ant Of A Nail", a fanfic starring Xenwa, Warrior Wprincess.)

Except I didn't use that

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,

Reading about digamma, its history of transformations seems comprehensive!

The symbol that looks like

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.)

Latin small letter l with bar?

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,

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} ̵ \) ]

This is a good thing

We need more people here who will show how to solve problems in language theory with two or three arrows.