Lambda - 概述
Lambda 演算 (Lambda Calculus) 是数学家 阿隆佐·邱奇 在 1930 年代发明的一套形式系统，它用非常简单的规则来定义计算、函数和应用。它的目标是探究“什么是可计算？”这一根本问题。
邱奇-图灵论题 The Church-Turing thesis
邱奇-图灵论题 (The Church-Turing thesis) 是计算机科学领域关于可计算性本质的核心假说，提出所有有效可计算函数均可由图灵机实现，常规编程语言具备完整的算法表达能力。该论题通过图灵机模型将数学中的”有效方法”概念形式化，但对”有效方法”本身未给出严格的数学定义。
起源
该论题源于1936年图灵在 《论可计算数及其在判定问题中的应用》 提出的图灵机模型，同时期邱奇通过 λ演算 (也就是我们今天的议题) 和 递归函数 理论描述可计算性。两人分别独立解决了希尔伯特判定性1问题，并证明各自模型的计算能力等价。
哲学思考
论题的哲学内涵涉及数学基础与计算边界问题，其思想源于对希尔伯特计划2的反思，并在哥德尔不完备定理3的背景下发展形成
[!attention] Lambda演算 vs. Lambda表达式 我们这里要讨论的是Lambda演算，它其实是编程语言中Lambda表达式的源头，但其本身并不服务于计算机语言，而是计算理论
Lambda演算の核心思想
一切皆函数 在 Lambda 演算中，所有东西都是函数。没有数字、字符串、布尔值这些基本类型——它们全都可以用函数的组合来表示。
我们将在接下来的几个文章里详细探讨并阐述我的个人理解
[[2025-12-20-Lambda - 1 基本定理]]