
文档教程【免费下载链接】learnxinyminutes-docsCode documentation written as code! How novel and totally my idea!项目地址https://gitcode.com/gh_mirrors/le/learnxinyminutes-docs点击查看免费下载本文基于开源仓库 learnxinyminutes-docs 中的西班牙语教程 es/lambda-calculus.md其英文原版为 lambda-calculus.md本仓库将该主题归类于 Algorithms Data Structures系统展开。λ 演算Cálculo Lambda由 [Alonzo Church] 于 20 世纪 30 年代提出被认为是世界上最小的编程语言它没有数字、字符串、布尔值或任何非函数数据类型却足以表示任何图灵机。读完本文你将掌握 λ 演算的三种基本构造、β-归约求值、丘奇编码Church numerals的布尔与自然数表示以及如何把表达式逐步压缩为更极简的 SKI、SK 与 Iota 组合子演算。一、λ 演算的三种基本元素λ 演算全部由三种元素构成变量variables、函数functions和应用applications。下表完整对应原文档的语法定义名称Nombre语法Sintaxis示例Ejemplo解释Explicación变量Variablenombre/namex一个名为 x 的变量函数Funciónλparámetro.cuerpo/λparameters.bodyλx.x以 x 为参数、以 x 为函数体的函数应用Aplicaciónfunciónvariable o función/functionvariable or function(λx.x)a以参数 a 调用函数 λx.x最基本的函数是恒等函数función de identidadλx.x它等价于普通数学记号f(x) x。其中第一个 x 是函数参数第二个 x 是函数体。说明在本仓库中λ 演算教程以多语言形式维护除西班牙语 es/lambda-calculus.md 与英文原版 lambda-calculus.md 外还提供了 中文版、法语版、葡萄牙语版 等翻译各版本核心内容保持一致便于对照阅读。二、自由变量Libres与约束变量Enlazadas区分变量是否被绑定是理解 λ 演算的第一步在函数λx.x中x 被称为约束变量variable enlazada因为它同时出现在函数体与参数位置参数声明约束了函数体内的同名出现。在λx.y中y 被称为自由变量variable libre因为它从未被预先声明游离于任何抽象之外。从实现角度看这一区分正是所有词法作用域语言的核心机制约束变量对应局部变量自由变量对应必须由外部环境提供的名称。后续 β-归约的替换规则也依赖于这一概念。三、求值β-归约β-Reduction求值通过β-归约完成其本质就是词法作用域内的替换sustitución de ámbito léxico求值表达式(λx.x)a时把函数体中所有出现的 x 替换为 a。基础归约示例(λx.x)a归约得到a(λx.y)a归约得到y因为 y 是自由变量替换不触及它还可以构造高阶函数funciones de orden superior——函数的返回值仍是函数(λx.(λy.x))a归约得到λy.a柯里化Currificación / Currying传统 λ 演算只支持单参数函数但通过柯里化技术可以表达多参数函数把f(x, y, z)改写为逐个接收参数、逐个返回函数的形式。(λx.λy.λz.xyz)等价于f(x, y, z) ((x y) z)有时λxy.cuerpo即λx.λy.cuerpo的缩写写法与完整嵌套形式互换使用二者语义完全一致。现代函数式语言如 Haskell 等中函数天然柯里化的设计理念正是源于此处。一个关键认知必须强调传统 λ 演算没有数字、字符或任何非函数数据类型。下面即将看到的布尔值与自然数全部是函数编码的产物而非内建类型。四、布尔逻辑用函数表示真与假λ 演算中没有 Verdadero/Falso甚至没有 1 或 0。取而代之的是两个特殊的二参数函数T表示为λx.λy.x选择第一个参数F表示为λx.λy.y选择第二个参数首先定义 if 函数IF若b为真则返回t若b为假则返回f。IF等价于λb.λt.λf.b t f借助IF可以定义基本布尔逻辑运算符a AND b等价于λab.IF a b Fa OR b等价于λab.IF a T bNOT a等价于λa.IF a F T注IF a b c本质上表示IF((a b) c)即IF依次应用于三个参数由于应用是左结合的b t f即(b t) f——把b当作选择器喂给它t和f。验证一下AND T F展开为IF T F F T F F而T F F (λx.λy.x) F F F结果正确。可见布尔值本质上是选择函数。五、自然数丘奇编码Números de Churchλ 演算中没有数字但可以用丘奇数Númeral de Church把自然数编码为函数。其思想是数字n表示把函数f应用n次即n λf.fn。因此0 λf.λx.x1 λf.λx.f x2 λf.λx.f(f x)3 λf.λx.f(f(f x))后继函数función sucesora要让丘奇数自增S(n) n 1定义S λn.λf.λx.f((n f) x)其含义是给定丘奇数n与函数f先对x应用n f即n次再额外应用一次f从而得到n1次应用。加法AGREGAR / ADD借助后继函数可以定义加法AGREGAR λab.(a S)b即对a反复施加后继函数b次得到a b。注英文原版写作ADD λab.(a S)b西班牙语版存在笔误(a S)n应以(a S)b为准中文版 同样使用正确形式。挑战Desafío尝试自己定义乘法函数提示乘法a × b可以理解为把b复制a份并叠加一个常见答案是MULT λab.λf.a (b f)。六、变得更小SKI、SK 与 Iota 组合子演算原文档在讲完丘奇数后进一步压缩 λ 演算本身展示如何用更少的原语表达一切。SKI 组合子演算Cálculo del combinador SKI设 S、K、I 为如下函数I x x恒等K x y x常函数丢弃第二个参数S x y z x z (y z)分配/替换规则可以把 λ 演算中的任意表达式转换为 SKI 组合子表达式只需三条转换规则λx.x Iλx.c Kc前提x未在c中自由出现λx.(y z) S (λx.y) (λx.z)以丘奇数 2 为例演示完整推导2 λf.λx.f(f x)先处理内层λx.f(f x)λx.f(f x) S (λx.f) (λx.(f x)) (规则 3) S (K f) (S (λx.f) (λx.x)) (规则 2、3) S (K f) (S (K f) I) (规则 2、1)于是2 λf.λx.f(f x) λf.(S (K f) (S (K f) I)) λf.((S (K f)) (S (K f) I)) S (λf.(S (K f))) (λf.(S (K f) I)) (规则 3)对第一个参数λf.(S (K f))继续转换λf.(S (K f)) S (λf.S) (λf.(K f)) (规则 3) S (K S) (S (λf.K) (λf.f)) (规则 2、3) S (K S) (S (K K) I) (规则 2、3)对第二个参数λf.(S (K f) I)λf.(S (K f) I) λf.((S (K f)) I) S (λf.(S (K f))) (λf.I) (规则 3) S (S (λf.S) (λf.(K f))) (K I) (规则 2、3) S (S (K S) (S (λf.K) (λf.f))) (K I) (规则 1、3) S (S (K S) (S (K K) I)) (K I) (规则 1、2)合并两部分2 S (λf.(S (K f))) (λf.(S (K f) I)) S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))若继续展开这个最终表达式会再次得到与丘奇数 2 等价的表达式——转换是保语义的这正是组合子演算作为 λ 演算等价形式的价值。SK 组合子演算SKI 还可以继续精简。注意到I SKK因为SKK x K x (K x) x因此可以用SKK替换所有I去掉 I 组合子得到只有 S 与 K 两个原语的SK 组合子演算。Iota 组合子SK 演算仍非最简。定义单参数组合子 ιι λf.((f S) K)可以仅用 ι 重构出 I、K、SI ιι K ι(ιI) ι(ι(ιι)) S ι(K) ι(ι(ι(ιι)))至此整个 λ 演算的能力被压缩进单一符号 ι——最小的追求走到了逻辑极限。这一系列从 SKI → SK → Iota 的压缩链条直观展示了组合子逻辑combinatory logic如何用极少的原语保持图灵完备性。七、本仓库中的文档组织与质量保障learnxinyminutes-docs 仓库以把文档写成代码、随代码讲解的方式维护这些教程。关于 λ 演算主题仓库内同时维护着英文原版 lambda-calculus.mdfrontmatter 中声明category: Algorithms Data Structures以及 es/lambda-calculus.md、zh-cn/lambda-calculus.md、fr/lambda-calculus.md、pt-br/lambda-calculus.md 等多语言版本各版本共用同一套作者署名翻译者单独记录于translators字段。仓库为每篇文章提供了规范化的 frontmatter 与风格约束CONTRIBUTING.md 要求代码行宽不超过 80 字符、优先用代码示例而非长篇论述、全篇使用 UTF-8 编码并定义了name、contributors、category、filename、translators等元数据字段非英文文章会继承英文版的 frontmatter 值。lint/frontmatter.py 中的extract_yaml_frontmatter负责从 Markdown 文件头部提取---包裹的 YAML 元数据validate_yaml_keys则校验文档只允许出现规定的键确保所有语种文章的元数据结构一致、可被站点生成器正确消费。如果你想在本地通读全文直接查看 es/lambda-calculus.md西班牙语或 lambda-calculus.md英文即可对照 中文版 可以快速消除语言障碍。八、进一步阅读建议原文档末尾给出了一系列进阶资料方向这里整理为纯文字指引不附外部链接《A Tutorial Introduction to the Lambda Calculus》λ 演算入门教程学术向经典 PDF 讲义康奈尔大学 CS 3110/CS 312 关于 λ 演算的复习讲义维基百科的 Lambda Calculus 词条含 β-归约、α-等价等严格定义维基百科的 SKI combinator calculus 词条维基百科的 Iota and Jot 词条单一原语的极简语言家族。建议按顺序阅读先吃透本文的三大元素与 β-归约再用丘奇编码动手实现加法与乘法完成文中的挑战最后沿着 SKI → SK → Iota 的推导亲手走一遍即可对可计算性理论的最小区块建立完整的直觉。赞分享文档教程【免费下载链接】learnxinyminutes-docsCode documentation written as code! How novel and totally my idea!项目地址https://gitcode.com/gh_mirrors/le/learnxinyminutes-docs点击查看免费下载相关推荐Learn X in Y Minutes 之 Go 语言实战指南从语法骨架到并发与 Web 编程Learn X in Y Minutes 之 Go 语言实战指南从语法骨架到并发与 Web 编程 本篇指南以 learnxinyminutes docs 仓库文档教程Jest Timer Mocks 完全指南用假定时器精确控制测试时间Jest Timer Mocks 完全指南用假定时器精确控制测试时间 导读 在 Jest 测试中 setTimeout 、 setInterval 等原生定文档教程Learn X in Y Minutes 之 SmallBASIC从语法速览到图形与 JSON 实战Learn X in Y Minutes 之 SmallBASIC从语法速览到图形与 JSON 实战 本指南基于 learnxinyminutes docs文档教程创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考