莱姆答还原（λ-reduction），文学-语言文字-语义学-莱姆答运算，类型论的一种对λ约束的变量逐一赋值并逐步消去λ的运算过程。与莱姆答抽象是相逆的过程，也写作“λ还原”。谓词在形式化表达和翻译时，可以通过莱姆答抽象得到符合谓词类型（见“两体类型论”）的表达式。例如，二元谓词“love”（爱）的莱姆答表达式：λxλy[love(y)(x)]，类型为〈e,〈e，t〉〉，其中x是主语论元，y是宾语论元。然而，类型为t的自然语句中，谓词的主语和宾语都是确定的，此时就需要将主语论元和宾语论元代入表达式为λxλy[love(y)(x)]中，除去λ抽象的部分，将自由变量x和y替换为类型为e的主语和类型为e的宾语，从而消去受λ约束的自由变量，将表达式的类型变成t，这样也就符合自然语句的类型。莱姆答还原的具体操作如下。在对自然语句“约翰爱玛丽”形式化表达和翻译时，需要对谓词“爱”的表达式λxλy[love(y)(x)]进行λ还原。