LSGX

# 程序与证明

http://www.idris-lang.org/
http://docs.idris-lang.org/en/latest/
https://github.com/edwinb
https://edwinb.wordpress.com
https://github.com/soimort
https://github.com/david-christiansen

-----------------------------------------------------------------------------------
Logic, Proof and Computation

The text  Logic, Proof and Computation  (233 pages, £15) is now available.

Order this book now direct from the publisher.  Logic, Proof and Computation will be available from other sites in 2015. You can download the programs for this book  here  (includes Shen executable for Windows 7). For Linux users, you can  download Shen  from this site.

Logic, Proof and Computation is designed as a multidisciplinary reader for students in computing, philosophy and mathematics.

Beginning with a review of formal languages and their syntax and semantics, Logic, Proof and Computation conducts a computer assisted course in formal reasoning and the relevance of logic to mathematical proof, information processing and philosophy.

Topics covered include formal grammars, semantics of formal languages, sequent systems, truth-tables, propositional and first order logic, identity, proof heuristics, regimentation, set theory, databases, automated deduction, proof by induction, Turing machines, undecidability and a computer illustration of the reasoning underpinning Gödel's incompleteness proof. The text is completely supported by free programs written to illustrate propositional and first-order reasoning, set theory, Turing machines and resolution.

Introduction

Lecture 1 Formal Languages
Natural and Formal Languages, Syntax and Backus-Naur Form, Some Terminology, Extended BNF, Beyond BNF, Further Reading

Lecture 2 Semantics and Proof
Model Theory, Proof Theory, Soundness and Completeness, The Semantics of Programming Languages, Further Reading

Lecture 3 Truth Tables and Propositional Calculus
Logic, The Syntax of Propositional Calculus, The Semantics of Propositional Calculus, Truth Tables and Tautologies, Further Reading

Lecture 4 Applications of Propositional Calculus
A Simple Argument, A More Complex Argument, Truth Functional Equivalence, Circuit Design and the Sheffer Stroke Function, SAT Solvers, Further Reading

Lecture 5 The Proof Rules of Propositional Calculus
Proof by Hypothesis, The Rules for &, The Rules for v, The Rules for =>, The Rules for <=>, The Rules for ~, Lemmas, Structural Rules, The Principle of Explosion, The Law of the Excluded Middle, Further Reading

Lecture 6 Building Propositional Calculus Proofs on a Computer
Why Use Computers?, The Provedit! Program, The Syntax of Provedit!, Modus Ponens, Modus Tollens, Double Negation, De Morgan’s Laws, Further Reading

Lecture 7 Heuristics of Propositional Calculus
Safe and Unsafe Rules, Getting Unstuck, Indirect Proof, Seeing Intermediary Steps, Semantic Checking and Computer Assisted Proof, Further Reading

Lecture 8 First Order Logic
Subject and Predicate, Relations, Functions and Complex Terms, Identity, Molecular Sentences, Quantifiers, Expressing Barbara in First Order Logic, The Syntax of First Order Logic, Further Reading

Lecture 9 Quantifier Proof in First Order Logic
all-right, all-left, all-right, all-left, The Syntax of First Order Logic in the Provedit! Program, Some Heuristics of Quantifier Proof, Further Reading

Lecture 10 Identity
= right, = left, Some Identity Proofs, Free Logic, Second Order Logic and the Identity of Indiscernables, Abstract Algebra, Boolean Algebra, Further Reading

Lecture 11 Formalisation in First Order Logic
Formalising ’All’, ’Every’, ’These’, Formalising ’A’, ’That’, and ’This’, Russell’s Theory of Definite Descriptions, ’Most’ and ’Many’, Measure, Adverbs, Expressions of Belief, Limitations of First Order Logic, Further Reading

Lecture 12 Set Theory
Sets, A Recursive Set Abstraction, Set Relations and Operations, Abstraction Free Set Theory,
The Syntax of AFST in Provedit!, Further Reading

Lecture 13 Pairs, Relations and Databases
Pairs and Tuples, Products, Relations and Functions, Codd’s Relational Agebra, SQL, Further Reading

Lecture 14 Taming the Complexity of Formal Proofs
Theorem Introduction, Tactics, Understanding the Shen Top Level, Defining New Functions, Tacticals, Further Reading

Anti-Realism, Strict Finitism, Conventionalism and Formalism, Further Reading

Lecture 16 Induction
Peano’s Axioms, Why Does Mathematical Induction Work?, Induction in Computer Science, The Heuristics of Inductive Proof, Two Inductive Proofs, Induction Schemes, Flawed Induction, The Sorites Paradox, Further Reading

Lecture 17 Turing Machines
The Entscheidungsproblem, Defining Computability, Turing Machines, Some Turing Machine Programs, A Turing Machine in Shen, The Universal Turing Machine, The Halting Problem, How is the Unsolvability Result Proved?, Formalising the Operation of a Turing Machine, Further Reading

Lecture 18 Resolution and Automated Deduction
The Prehistory of Automated Deduction, The Modern Period, Resolution, Clause Form, Resolution in Propositional Logic,
Learning Resolution in Shen, Further Reading

Lecture 19 Resolution and First Order Logic
Prenex form, Skolemisation, Unification, Factorisation, Resolution in First Order Logic, Using Shen to Learn First-Order Resolution, Further Reading

Lecture 20 Gödel and the Limits of Proof
Gödel's Incompleteness Theorem, Provability as a Predicate, The Significance of Gödel's Result, Further Reading

Index
Select Bibliography

-------------------------------------------------------------------------

{-
Turing complete, or not Turing complete: that is the question:
Whether 'tis nobler in the machine to suffer
The undecidability of a paradoxical recursion,
Or to take proofs against a sea of calculi,
And by opposing halt them?

-- soimort's soliloquy
-}

• §0 前言
• §1 从计算到程序
• §2 语言的巴别塔
• §3 程序即证明
• §4 程序非证明
• §5 结语

## §0 前言：关于一部传记文学，以及未来的计划

* * *

* * *

“数百年后，必有用我此说者！”我在心里悲怆地喊出，回答我的是无边的暗夜和沉默。

* * *

## §1 从计算到程序：图灵完备的神话

……数学，与众多理性科学一样，以一门不严谨的计算技巧之名而诞生。在经历了重重危机之后，人们终于认识到使其公理化的必要性，作为终极的自然科学——物理学理论的基础、一门“元科学”的数学，就这样终于成为建立于形式化逻辑之上的一个严密理论体系。比起现世先验知识的总结，它更加体现出人类智慧的结晶；愈是暴露出人类直觉的模糊与不可靠性（如同非欧几何、ZFC公理体系显示出的与人类感官直觉背道而驰的表象），愈是能彰显出逻辑学的价值。

——某未完成的计算科学史原稿

A：FlooP 是一种编程语言吗？

B：是的，因为它是图灵完备的。

A：我可以在 FlooP 语言里实现 X 功能吗？

B：当然可以，它是图灵完备的，理论上你可以用它实现任何功能！

A：BlooP 是一种编程语言吗？

B：不是，因为它不是图灵完备的，它无法实现任意计算。

* * *

# Row 1

> [-] >> [-] > [ <+ <<+ >>>- ] <<< [ >>>+ <<<- ]
>> ----- ----- ----- ----- ----- ----- --- #O
<< [-] > [-] > [ <<+ >+ >- ] << [ >>+ <<- ] +
> [ <- > [-] ]
< [ >>>
> [-] >> [-] > [ <+ <<+ >>>- ] <<< [ >>>+ <<<- ]
>> ----- ----- ----- ----- ----- ----- --- #O
<< [-] > [-] > [ <<+ >+ >- ] << [ >>+ <<- ] +
> [ <- > [-] ]
< [ >>>
> [-] >> [-] > [ <+ <<+ >>>- ] <<< [ >>>+ <<<- ]
>> ----- ----- ----- ----- ----- ----- --- #O
<< [-] > [-] > [ <<+ >+ >- ] << [ >>+ <<- ] +
> [ <- > [-] ]
< [ >>>
> [-] >> [-] > [ <+ <<+ >>>- ] <<< [ >>>+ <<<- ]
>> ----- ----- ----- ----- ----- ----- --- #O
<< [-] > [-] > [ <<+ >+ >- ] << [ >>+ <<- ] +
> [ <- > [-] ]
< [ >>>
<<<< <<<< <<<< <<<<
[-] +
>>>> >>>> >>>> >>>>
<<< - ] <
<<< - ] <
<<< - ] <
<<< - ] <


x == "OOOO"


var results = from c in SomeCollection
where c.SomeProperty < 100
select new {c.SomeProperty, c.OtherProperty};


* * *

* * *

## §2 语言的巴别塔：图灵完备的终结？

——《创世记》

1. 从一种语言出发，可以得到另一种语言吗？

3 + 7 =

(+ 3 7)


3 + 7


mov eax, 3


(define ego (lambda () (ego)))


$awk 'BEGIN{for(;;);}'  $ awk 'function _(){_()}BEGIN{_()}'


* * *

2. 语言可以作为另一种语言的载体吗？

* * *

3. 程序语言可以实现另一种程序语言吗？

* * *

C++ 则是另外一个世界。它的模板元编程特性无限制地剥削了编译期间的预处理能力：（这个例子来自于 Stack Overflow）

template <int I>
struct Infinite {
enum { value = (I & 0x1)? Infinite<I+1>::value : Infinite<I-1>::value };
};
int main() {
int i = Infinite<1>::value;
}


error: template instantiation depth exceeds maximum of 900
(use -ftemplate-depth= to increase the maximum)
instantiating ‘struct Infinite<901>’


（你可能听说过 Haskell 的类型系统与 C++ 模板存在着相似性 这种说法。既然两者同样都实现了图灵等价的计算模型，那么这件事也就不难理解了。）

* * *

1、它可以用来实现一切可形式化验证的正确算法，但无法实现你自己都不知道是否停机的算法；

2、它可以用来实现永不终止但持续执行有效计算的软件，如一个操作系统、一个网站；但它无法实现空的死循环、爆栈而不产出有效数据输出的递归，或其他一切任何你认为“无用却不停机”的计算。

* * *

* * *

* * *

## §3 程序即证明

Mort 是狐猴。

——某有效但不一定可靠的一阶逻辑推理

* * *

JavaScript 的类型之“弱”则主要以另一种方式体现：隐含类型转换的不可预知性。

1 + "2"


Robert Harper 说：最近若干年世界上每一种新出现的程序语言，都在变得更像 ML。我想，不单是 Scala、F#、Rust 和 Swift 这样的新兴静态语言，即便是最传统的动态语言如 Lisp，也早就在向“静类型检查”和“针对类型编译优化”这两个方向发展：从 Common Lisp，Typed Racket，直到近年的 Typed Clojure；至于 Python 之父向来推崇 Haskell，最近又提出要在 Python 中吸收 mypy 类型检查的记号语法，大概已经 广为人知 了。

* * *

x : Int

y : String


f : Int -> Int


--定义

Mort : 居住于[马达加斯加]的[狐猴]


--定义

Mort : 居住于[火星]的狐猴


z : Int
z = f x


z : String
z = f x


z : Int
z = f y


f : (Int, String) -> Int

z : Int
z = f (x, y)


f : Int -> (String -> Int)

z : Int
z = (f x) y


f : Int -> String -> Int

z : Int
z = f x y


f : Int -> String -> Int
g : (Int -> String) -> Int


f : (Int -> String) -> Int -> String


f : Int -> String -> (Int, String)
f x y = (x, y)


f : (Int, String) -> Int
f (x, y) = x


【练习1】 实现如下函数，取出值对中的第二个值：

f : (Int, String) -> String


* * *

f : (Int -> String) -> Int -> String


f : (Int -> String) -> Int -> String
f x y = x y


f2 : (Int -> Bool) -> Int -> Bool
f2 x y = x y

f3 : (String -> Int) -> String -> Int
f3 x y = x y

f4 : (String -> String) -> String -> String
f4 x y = x y


f : {p, q : Type} -> (p -> q) -> p -> q
f x y = x y


apply : (a -> b) -> a -> b
apply f a = f a


f : {p : Type} p -> p


id : a -> a
id x = x


f : {p, q : Type} p -> q


【思考1】 能否实现这样一个通用的函数？

f : {p, q : Type} -> (p -> q) -> q -> p


* * *

$P \to Q, P \vdash Q$

modus-ponens : ∀ {a b} {P : Set a} {Q : Set b} → (P → Q) → P → Q


modus_ponens : {p, q : Type} -> (p -> q) -> p -> q


modus_ponens : {p, q : Type} -> (p -> q) -> p -> q
modus_ponens x y = x y


modus_ponens = apply


modus_ponens x = x


modus_ponens = id


【练习2】 证明肯定前件的另一种书写形式：

modus_ponens' : {p, q : Type} -> p -> (p -> q) -> q


【练习3】 证明 假言三段论 （ hypothetical syllogism ）：

$(P \to Q), (Q \to R) \vdash (P \to R)$

hypo_syllogism : {p, q, r : Type} -> (p -> q) -> (q -> r) -> p -> r


* * *

f : Int -> String -> (Int, String)


f : {p, q : Type} -> p -> q -> (p, q)


$P, Q \vdash (P \land Q)$

conjunction : {p, q : Type} -> p -> q -> (p, q)
conjunction x y = (x, y)


conjunction : {p, q : Type} -> p -> q -> Pair p q


【练习4】 证明 合取消去 （ simplification ）：

$(P \land Q) \vdash P$

simplification : {p, q : Type} (p, q) -> p


* * *

$\neg \neg P \vdash P$

$P \vdash \neg \neg P$

$\neg P$

f :  p -> _|_


$P \to \bot$

f : {p : Type} -> p -> (p -> _|_) -> _|_


f : {p : Type} -> p -> (p -> _|_) -> _|_
f x y = y x


Idris 标准库中为了证明的易读性，定义了 Not 函数，它将任意一个类型 a 映射到函数类型 a -> _|_ （即命题 a 为假）后返回：

Not : Type -> Type
Not a = a -> _|_


double_neg_intro : {p : Type} -> p -> Not (Not p)
double_neg_intro x y = y x


$P \vdash \neg \neg P$

【练习5】 证明 否定后件 （ modus tollens ）：

$P\to Q, \neg Q \vdash \neg P$

modus_tollens : {p, q : Type} -> (p -> q) -> Not q -> Not p


modus_tollens : {p, q : Type} -> (p -> q) -> (q -> _|_) -> p -> _|_


【思考2】 能否像上面一样，完成对于双重否定消去（double negation elimination）的证明？（无论是直接用 Idris 来实现下面的函数也好，改用等价的 Agda 或 Haskell 也好；不妨先尝试一下。）

$\neg \neg P \vdash P$（双重否定消去）

double_neg_elim : {p : Type} -> Not (Not p) -> p
-- Expands to:
-- double_neg_elim : ((p -> _|_) -> _|_) -> p


* * *

* * *

data Nat : Type where
Z : Nat
S : Nat -> Nat


data Nat = Z | S Nat


S (S (S (S (S (S (S Z))))))


plus : (n, m : Nat) -> Nat
plus Z right        = right               -- 定义1
plus (S left) right = S (plus left right) -- 定义2


$plus\ (S\ (S\ (S\ Z)))\ (S\ (S\ Z))$

$=S\ (plus\ (S\ (S\ Z))\ (S\ (S\ Z)))$（根据定义2）

$=S\ (S\ (plus\ (S\ Z)\ (S\ (S\ Z))))$（根据定义2）

$=S\ (S\ (S\ (plus\ Z\ (S\ (S\ Z)))))$（根据定义2）

$=S\ (S\ (S\ (S\ (S\ Z))))$（根据定义1）

$\forall{n}{\in}\mathbf{N}, 0+n=n$

$\Pi_{(n:{\mathbb N})}\ plus\ Z\ n=n$

plusReduces : (n : Nat) -> (plus Z n = n)


plusReduces : (n : Nat) -> (plus Z n = n)
plusReduces n = refl


* * *

wtf : (n : Nat) -> lte (S Z) n = True
wtf (S k) = refl


* * *

Naive 这件事最初说的是朴素集合论（naive set theory）。我们都听说过那个著名的理发师悖论：

$\text{Let } R = \{ x \mid x \not \in x \} \text{, then } R \in R \iff R \not \in R$

1) 罗素对“ 类型 （type）”这一概念的原始定义： 使命题函数具有意义的范围 。

f : {p, q : Type} -> (p -> q) -> p -> q


2) 我们有时会需要针对 所有 命题量化。（即允许 非直谓性 的存在）

3) 命题和类型的同一性。或者用通俗的话说，命题即类型，两者可以完全等同。

T. Coquand 的选择是取 2) 而舍 3)。换言之， 命题和类型不可以完全等同 。他提出了用“小类型”和“大类型”的概念对类型加以区分，这条路引出了所谓的构造演算（ Calculus of Constructions ），其中包含五个基本概念：

1. 证明 ：类型为命题的项。
2. 命题 ：又称作小类型。
3. 谓词 ：返回命题的函数。
4. 大类型 ：谓词的类型。
5. 大类型的类型 T。

*universe> :t Type
Type : Type 1


myid : (a : Type) -> a -> a
myid _ x = x

idid : (a : Type) -> a -> a
idid = myid _ myid


* * *

1. 所有的函数必须被完整地实现，即针对每一个可能的值都有定义；
2. 递归必终止（对应到命令式语言中，则循环必终止）；编译器有权拒绝一切它无法判断是否停机的计算。

* * *

## §4 程序非证明

——Robert Harper《圣三位一体》

ML 程序员常常会对 Haskell 默认情况下不检查函数定义完整性这件事感到 无法理解 。即使是在现实的编程中，确保所有函数被完全地定义也是一件重要的事情：和类型安全同样的道理，尽可能地把缺陷扼杀在编译时；一个 missing case 可能会导致运行时出现无法预料的错误。

Idris 是种深受 Haskell 影响的语言。但正如许多人所见，一种能够被用于形式化证明的语言，默认行为不是 total 应该是不科学的，它导致我们足以完成上一节提到的那个关于 ∀n∈ℕ, 1≤n 的错误证明。至于它为何这样设计，这里有一个 冗长的解释 ，在此略过。在 Idris 里，我们可以直接调用编译器选项 --total ，或使用开关

%default total


total
wtf : (n : Nat) -> lte (S Z) n = True
wtf (S k) = refl


$M$  (   n   )   =   {   n     10   ,   i   f   n   >   100   M   (   M   (   n   +   11   )   )   ,   i   f   n     100

total
f91 : (n : Nat) -> Nat
f91 n with (n > 100)
| True = n - 10
| False = f91 (f91 (n + 11))


  Main.f91 is possibly not total due to: with block in Main.f91


（注意，在这里，我们仅仅用 “partial” 这个词来表达“non-total”的含义：它和程序语言中其它语境下所说的 partial，诸如“partial application”“partial evaluation”并无直接关联。）

partial
f91 : (n : Nat) -> Nat
f91 n with (n > 100)
| True = n - 10
| False = f91 (f91 (n + 11))


* * *

codata Partial a = Later (Partial a) | Now a


Idris 中，一个 codata 是一个被惰性求值的数据结构。对于 Partial Monad 而言，还需要一些最基本的定义：

instance Functor Partial where
map f (Now x) = Now (f x)
map f (Later xs) = Later (map f xs)

instance Applicative Partial where
pure = Now

f <$> (Later xs) = Later (f <$> xs)
(Now f) <$> (Now x) = Now (f x) (Later fs) <$> x = Later (fs <$> x) instance Monad Partial where (Now a) >>= k = k a (Later d) >>= k = Later (d >>= k)  这个 Partial Monad 的意义何在呢？用简单的话讲，就是：每执行一次计算，我要么证明它是有生产率（productive）的（ Later ），要么就让它终止计算得到最终结果（ Now ）。 “生产率（productivity）”的概念对于 total functional 编程来说非常重要。这么做意味着你可以读取和输出无限的 stream（比如文本文件），对每一个数据执行可验证的计算，而不必担心“图灵完备”这件事情破坏了计算的可靠性：因为你知道，你的真实计算（或证明）本身是图灵非完备的，它必然停机给出结果；而把每一次这样的计算放到一个 Partial Monad 中，你又具有了不停机持续完成计算的能力。同理，你可以实现一个操作系统、一个 Web server，它们的每一步纯计算都是 proof-carrying 的可验证代码；然而作为一个保持生产率的整体，它总是源源不断地向外界贡献它的计算能力。 当然，意义这件事情本是人为赋予的。一个 Web server 挂在那里运行，即使什么计算也不做也不停机，它分分钟都是有贡献的（我想没有人能否认这一点）。同样，你可以认为一个递归函数每当完成一步计算，就算是为科学界贡献了一点东西，比如又把圆周率的计算推进了若干位；你也可以认为把一个不知道是否停机的证明持续验证下去是一件毫无生产率的事情。假设我不关心前面所说的 McCarthy 91 函数是否停机，我认为它每做了一步递归，就是有贡献的，至少它成功地让我的机器发热了；那么，把计算放到 Partial Monad 里实现，我们就得到了 total 版本的 McCarthy 91 函数实现： total f91' : Partial Nat -> Partial Nat f91' (Later p) = Later (f91' p) f91' (Now n) with (n > 100) | True = Now (n - 10) | False = Later (f91' (Later (f91' (Now (n + 11)))))  注意它作为一个整体的实现，仍然是 total 的：你不能让它任意地去调用另一个 partial 函数，或者直接递归调用自身而不通过 Partial Monad 来保障其生产率；类型系统将会阻止你这么去做。于是，我们所使用的语言特性被限制在了 total functional 的范围内，却实现了通常只有图灵完备语言才能实现的计算。理解这一点是一步质的飞跃：从“ 我不确定是否停机 ”的、处于混沌状态的图灵完备编程，到“ 我确信它一定会停机 ”的计算和“ 我知道什么是有用的不停机 ”的计算严格区分的图灵非完备编程。 所以，图灵完备计算有哪些是图灵非完备计算所做不到的？这就是我的答案： 你既不能确定它是否停机、又不能确定它有没有用的。 Total functional 是对“程序如证明”这件事情正确性的保证：你无法写出一个不终止的递归函数，也就无法写出任何逻辑上不自恰的证明。Partial Monad 严格地将需要被保障正确性的程序逻辑和“有用的”不停机的计算过程分隔开，你需要显式地告诉类型系统：这段程序虽然我无法知道它会否停机，但我保证它一定是有用的！它在不停地计算下一位圆周率，或者在跑一个网站，或者甚至就是我服务器上运行的操作系统，直到宕机之前我都不打算让它停下来；如此种种。 * * * 现在，我们终于可以回到之前在第2章里提出的问题上了： 能否以图灵非完备的编程方式，去实现一个图灵完备语言的解释器呢？ 在理解了“程序即证明”和 total functional 编程的意义之后，你会发现：“用图灵非完备语言来实现图灵完备语言”这件事本身，已经不足以成为我们的目的了。因为以图灵非完备的能力，我们仍可实现任何已知的有用的程序；更重要的是，它可以通过类型和逻辑的同构性，借助类型检查确实保证程序实现的正确性——假如我们认真严肃地对待“软件功能性规范”这件事的话。当然，若是能用它来实现一个图灵完备的计算模型，也许更容易让人信服它的“有用性”。 接下来，我们将以 total functional 的方式在 Idris 中实现一个基本的 无类型λ演算 解释器，而它是图灵完备的。它的核心实现不过13行，加之以数十行辅助的类型定义。比起废话连篇，实际的编程总是要简单许多！ * * * Idris 设计的初衷之一是用于构建可验证的嵌入式领域专有语言， 这里 介绍了一个对简单类型λ演算 （simply typed lambda calculus）的解释器实现（ 视频 ）。注意到简单类型λ演算并不是图灵完备的，它的主要作用体现在函数式语言的类型系统实现上。而我们在这里将要实现的是 无类型λ演算 （untyped lambda calculus），它可以作为一个图灵完备语言的基础。 本文探讨的主要话题是“程序和证明”，故其篇幅不足以容纳一篇解释器的入门教程。关于怎样实现无类型λ演算的基础知识，请参见 Matthew Might 的 博客 或王垠的 博客；注意这两篇文章里的实现用的是 Scheme 或 Racket。实际上无类型λ演算解释器的基本构造都是大同小异的，因为它实在太简单了。 这个在 Literate Idris 里用 total functional 方式实现的无类型λ演算解释器如下： 导入标准库里的 Data.SortedMap 数据类型和之前定义的 Partial Monad > import Data.SortedMap > import Partial 默认使用 total > %default total λ演算里表示名字的符号类型 > data Symbol = Symbol_ String 表达式的定义：一个变量，一个λ，或一个函数应用 > data Expr = Var Symbol > | Lambda Symbol Expr > | App Expr Expr 函数的定义：一个表达式 > data Function = Def Expr Show instance > instance Show Symbol where > show (Symbol_ str) = str > instance Show Expr where > show (Var sym) = show sym > show (Lambda sym expr) = "\\" ++ show sym ++ "." ++ show expr > show (App expr1 expr2) = show expr1 ++ " " ++ show expr2 > instance Show Function where > show (Def expr) = show expr > mutual 环境的定义：一个将 String 映射到 Value 的记忆体（使用 SortedMap 实现） > data Environment = Memory (SortedMap String Value) 值的定义：一个包含函数和环境的闭包，或一个异常（错误） > data Value = Closure Function Environment > | Exception String Show instance > instance Show Value where > show (Closure fun env) = show fun > show (Exception str) = "Exception: " ++ str > mutual 在环境中解释表达式（即执行求值） > ||| Evaluate an expresssion in an environment. > ||| @ expr the expresssion > ||| @ env the environment > total > interp : (expr : Expr) -> (env : Environment) -> Partial Value 对于一个变量，直接从记忆体中返回其名字对应的值；若不存在，则返回一个异常 > interp (Var sym) (Memory m) with (lookup (show sym) m) > | Just val = Now val > | Nothing = Now (Exception "undefined symbol") 对于一个λ，返回一个由其代表的函数和当前环境组成的闭包 > interp (Lambda sym expr) env = Now (Closure (Def (Lambda sym expr)) env) 对于一个函数应用，对前表达式和后表达式在当前环境下进行求值，并执行应用（有生产率的递归） > interp (App expr1 expr2) env = Later (app (interp expr1 env) (interp expr2 env)) 将一个值应用到另一个值（即函数应用） > ||| Apply a function to its argument. > ||| @ f the function > ||| @ a the argument > total > app : (f : Partial Value) -> (a : Partial Value) -> Partial Value 应用被延迟（有生产率的递归） > app (Later f') a = Later (app f' a) 将值代入记忆体，并解释表达式 > app (Now (Closure (Def (Lambda sym expr)) (Memory m))) a = interp expr (Memory (insert (show sym) !a m)) 返回一个异常 > app (Now (Exception str)) a = Now (Exception str) 其它情况下不合法（构造错误的闭包），返回一个异常 > app (Now _) a = Now (Exception "malformed closure") 初始环境 > ||| Initial environment. > env0 : Environment > env0 = Memory empty  至此，我们已经完成了这个无类型λ演算解释器的实现，可以用它来完成一些简单的示例了。 【例1】 归约：$λx.x=λx.x$定义： expr1 : Expr expr1 = Lambda 'x (Var 'x)  求值： *UntypedLambdaTotal> interp expr1 env0 Now (Closure (Def (Lambda (Symbol_ "x") (Var (Symbol_ "x")))) (Memory Empty)) : Partial Value *UntypedLambdaTotal> show$ interp expr1 env0
"\\x.x" : String


【例2】 归约：

$λx.x\ λa.a=λa.a$

expr2 : Expr
expr2 = App (Lambda 'x (Var 'x)) (Lambda 'a (Var 'a))


*UntypedLambdaTotal> show $interp expr2 env0 "\\a.a" : String  【例3】 归约：$((λf.λx.f\ x)\ λa.a)\ λb.b=λb.b$定义： expr3 : Expr expr3 = App (App (Lambda 'f (Lambda 'x (App (Var 'f) (Var 'x)))) (Lambda 'a (Var 'a))) (Lambda 'b (Var 'b))  求值： *UntypedLambdaTotal> show$ interp expr3 env0
"\\b.b" : String


【思考3】 能否归约下式？为什么？

$λx.(x\ x)\ λx.(x\ x)$

expr4 : Expr
expr4 = App (Lambda 'x (App (Var 'x) (Var 'x)))
(Lambda 'x (App (Var 'x) (Var 'x)))


* * *

Partial 版本的实现：（对比）

（以上代码在 Idris 0.9.14.2 中编译通过）

* * *

## §5 结语：未完成的 Q.E.D.

Q.E.D.

### LSGX

08/01
0
0
Dafny与程序验证

B大以前写过一个怎样写出没有 bug 的程序：程序证明的简单例子 ，是用Idris写的，我也来写一个，不过方法不太一样。 Dafny是MSR开发的程序设计语言，它混合了OOP和FP编程范式，并且自带程序验...

2017/10/21
0
0

Coq 是一款交互式证明辅助工具，采用OCaml开发。Coq提供一套证明系统，可以编写证明，检查证明。Coq也提供一套形式化语言，可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明（比如...

2016/07/29
812
0

MrYuZixian
03/29
845
11

Albatross 是一门编程语言： 静态验证：可以开发程序和算法，证明在 Albatross 是正确的 证明助手：任意数学理论都可以在 Albatross 表述或者证实 理论证明：包括一个证明引擎 函数式，命令式...

2015/08/11
226
0

1. 网页加载速度更快 在网站中使用CDN技术最直接的一个好处就是它可以加快网页的加载速度。首先，CDN加速的内容分发是基于服务器缓存的，由于CDN中缓存了不少数据，它能够给用户提供更快的页...

42分钟前
7
0

symbiochina88
53分钟前
4
0

SOM-TL437xF是一款广州创龙基于TI AM437x ARM Cortex-A9 + Xilinx Spartan-6 FPGA芯片设计的核心板，采用沉金无铅工艺的10层板设计，适用于高速数据采集和处理系统、汽车导航、工业自动化等领...

Tronlong创龙
53分钟前
4
0

好程序员Java学习路线分享MyBatis之线程优化，我们的项目存在大量用户同时访问的情况，那么就会出现大量线程并发访问数据库，这样会带来线程同步问题，本章我们将讨论MyBatis的线程同步问...

59分钟前
6
0
IDEA 自定义方法注解模板

IDEA 自定义方法注解模板 1、使用效果 /*** 计算交易费用* @Author wangjiafang* @Date 2019/9/11* @param feeComputeVo* @return*/@PostMapping("/v1/fee_compute")public ApiResp......

6
0