multiletter names in lambda calculus

Question

First, I am new to TeX and use it only for mathematical expressions. IMHO the most striking feature is that TeX does not respect whitespaces.

1. In lambda calculus, application is denoted by juxtaposition. In programming languages based on lambda calculus (ML, Haskell) names may be several letters long, therefore, to separate names in application, a whitespace is placed between names. I want to use function names from standard libraries of those programming languages, therefore I can not just give up multiletter names. Currently I use “\ ” in application, but it seems hackish to me and clutters the code. What is the best way to do this? Example: You can take just any functional code, like $foldr\ f\ z\ (x:xs) = f\ x\ (foldr\ f\ z\ xs)$.

2. BTW, is it regular in lambda calculus to embrace multiletter names in “operatorname”?

Answer 1

It's not quite clear what symbols should be followed by a space and what not.

Something like

\newcommand{\lname}[1]{\mathop{\kern0pt\mathit{#1}}}

and

$\lname{foldr}\lname{f}\lname{z}(x:xs) =
  \lname{f}x(\lname{foldr}\lname{f}\lname{z}xs)$

might give good results. In other words, put each symbol you want to be spaced as argument of \lname. One might choose a different name for it: \? for example. It's quite hard to think how to render such formulas automatically, without explicit markup.

A similar effect as Andrew Stacey's can be obtained in standard LaTeX: the following lines go in the preamble

\newenvironment{lambdac}
  {\catcode` =12 \setupspace
   \makeordinary{:}% to make the colon an ordinary symbol
   %%% possible other \makeordinary declarations
   $\mathgroup0 }
  {$}
{\catcode` =\active\gdef\setupspace{\def {\;}}}
\makeatletter
\newcommand{\makeordinary}[1]{\@tempcnta=\mathcode`#1
  \@tempcntb=\@tempcnta
  \divide\@tempcntb by "1000
  \multiply\@tempcntb by "1000
  \advance\@tempcnta by -\@tempcntb
  \mathcode`#1=\@tempcnta}
\makeatother

In the document one can use

\begin{lambdac}
foldr f z (x:xs)=f x (foldr f z xs)
\end{lambdac}

One should put spaces only where they must appear in the output.

Note: the space has mathcode "8000, but this mathcode is ignored when the space has category code different from 11 or 12. The indirect definition of the active space avoids a global definition that could interfere with the \verb command.

Note: the \makeordinary macro strips off the first hexadecimal digit from a mathcode.

Result:

Answer 2

I've struggled with the same thing myself, and ended up with two possible solutions; first of which is basically egreg's solution (though you could just make the functions straight to macros, ie. \foldr). The other one is making math-mode obey spaces, but that has its own problems.

In the end, you basically won't save any typing with either of those.

To expand a little, what I've done is to define macros (these are in plain-format, latex-format would look different):

\def\defun#1{\mathop{\hbox{\it#1}}} % define functions as math operators,
  % so they get the spacing (note: not a "full" space, but a '\,'-space.)
\def\foldl{\defun{foldl}}
\def\foldr{\defun{foldr}}
\def\map{\defun{map}}
\def\filter{\defun{filter}}
\def\head{\defun{head}}
% etc. Silly, I know.
\def\f{\mathop f} % I don't want to remove the math italic kerning from 'f',
                  % because it has some additional space
$$ \foldr \f z (x:xs) = \f x (\foldr \f z\, xs) $$
% Note: I didn't want to remove the spacing of ':', and also, I used
% a manual spacing ('\,') to separate parameters.
\bye

The output looks like this:

It's a little tedious, but I think it looks good.

Answer 3

The semantic package can be helpful here. Among other things, semantic provides a reserved words feature that allows you to do the following:

% Preamble:
\usepackage{semantic}
\reservestyle{\concretesyntax}{\mathtt}
\concretesyntax{let[let\;],in[\;in\;]}

% Later:
$\<let> x = 5 \<in> x$

Produces this image:

You could define foldr, f, etc the same way (possibly exchanging \mathtt for something else).

Beyond that, semantic provides ligatures which provide a way to fix the spacing of : and .. (Both should have a space after, but not before.)

% Preamble:
\mathlig{:}{\!:}
\mathlig{.}{.\:}

% Later:
\lambda x: nat. x + 1

Produces this image:

Note: These styles attempt to mimick those from John Mitchell's textbook Foundations for Programming Languages. (Strangely enough, the formatting in my physical copy of his book differs from the downloadable chapter online, so keep that in mind.) In my opinion, my methods above do a much better job of reproducing his formatting than egreg's answer, which destroys spacing around : and removes italics on the variable names.