如何输入 lambda 表达式？

Question

如果点前始终没有空格，而点后有一些空格，我们可以使用\ldotp。例如，

\documentclass{amsart}

\begin{document}
\[
\lambda x\ldotp M\to((\lambda x\ldotp M)N).
\]
\end{document}

数学环境中的输出.会产生一个点，其前后没有空格。我们还可以将命令定义为数学运算符或关系，以产生（下）点。

\documentclass{amsart}
\makeatletter
\DeclareRobustCommand\dotbin{\mathbin{.}}
\DeclareRobustCommand\dotrel{\mathrel{.}}
\makeatother

\begin{document}
\[
\begin{array}{l}
\lambda x\ldotp M\to((\lambda x\ldotp M)N)\\
\lambda x.M\to((\lambda x.M)N)\\
\lambda x\dotbin M\to((\lambda x\dotbin M)N)\\
\lambda x\dotrel M\to((\lambda x\dotrel M)N).
\end{array}
\]
\end{document}

顺便说一句，我正在编写一个包含和的\dotbin包\dotrel。

λ 演算中点的一些历史

据我所知，学者们在lambda演算中使用的点有三种：第一种是产生的点\ldotp；第二种是产生的点.；第三种是\dotbin最早引入lambda演算的Church所使用的产生的点。

我认为第三种解释是正确的。教堂 1932，点也用于其他情况（参见第 356-358 页教堂 1932）。

事实上，丘奇从第 10 页借用了罗素和怀特黑德 1910（第一卷）。

此外，罗素和怀特黑德从皮亚诺 1889。皮亚诺把它当作某种括号。

嗯，在所有这些中，它的作用就像一些与产生的点相同的运算符\dotbin。

Answer 1