淺嘗The Little Prover一書, 重逢Chez Scheme

書開篇之前說, 本書的目標的一個例子: 證明(reverse (reverse x))對於任何列表x, 結果總是x.

(安裝Chez Scheme的200字請看最後)

書剛開始, 就用到一個scheme中沒有的函數atom和equal, 用中文定義應是如下:

注: 多謝 @張砸鍋 指正, 下面的"為空?"不正確, 名稱應該是"不是非空列表?". 原文用atom一詞, 就不直譯了. 鑒於似乎不影響本文後面的例子, 恕我不一一糾正了.

(define 為空?n (lambda (列表)n (if (atom? 列表)n niln t)))nn(define 相等?n (lambda (甲 乙)n (if (equal? 甲 乙)n tn nil)))n

書的第一個例子是在甲乙的值未知時, 對下面表達式求值

(相等? 那個啥 (為空? (cons 甲 乙))) n

(cons 甲 乙) 不論甲乙值為何, 都不會為空, 因此(為空? (cons 甲 乙))返回nil. 而(相等? 那個啥 nil)顯然返回nil, 因此這個表達式的值必定是nil.

這裡"(為空? (cons 甲 乙))肯定返回nil"被認為是Axiom(公理). 由這個公理推導出表達式的值.

第八頁列出了在Scheme"世界"里與cons相關的幾個公理:

(定義定律 cons不為空 (甲 乙)n (相等? (為空? (cons 甲 乙)) nil)n(定義定律 car/cons (甲 乙)n (相等? (car (cons 甲 乙)) 甲)n(定義定律 cdr/cons (甲 乙)n (相等? (cdr (cons 甲 乙)) 乙)n

之後就是equal相關的(交換律, 自身相等). 接下去是一系列基於這幾個定律的推導演繹. 而推導演繹法則(?不知說法是否恰當)本身被定義為如下:

對定律 (定義定律 名稱 (x1, x2, ...xn) 定律內容), "定律內容"中的x1~xn可以被任何表達式e1~en替換, 得出的新定律只要符合格式(相等? p q)或者(相等? q p), q就可以被置換為p.

舉例如下:

之前的定律car/cons

(定義定律 car/cons (甲 乙)n (相等? (car (cons 甲 乙)) 甲)n

可以作用於下面表達式:

(為空? (car (cons (car a) (cdr b))))n

只要把定律內容"(相等? (car (cons 甲 乙)) 甲)", 把"甲"替換為(car a), "乙"替換為(cdr b)之後就得出:

(相等? (car (cons (car a) (cdr b))) (car a))n

根據推導法, (car (cons (car a) (cdr b))) 等同於 (car a), 因此表達式等同於

(為空? (car a))n

看起來有些繞, 因此作者提供了輔助推導工具the-little-prover/j-bob. 第一章完(共十章).

感覺上是把定理以及推導的方法用代碼表達, 進而賦予了程序證明定理的能力.

為了運行書中的代碼, 決定裝Chez. 上次用好像還是在學校機房, 因為當時只有Petite Scheme是免費可以裝在個人機器, 而Chez還是商業軟體. 幾年過去, Dybvig教授離職去了思科, 而Chez Scheme隨後開源了(cisco/ChezScheme). 今天嘗試了下載9.5版, 在Mac上編譯生成了Petite和Chez(中間碰到了這個問題).

運行後的提示即眼熟又生疏. 個人的力量畢竟有限, 不知道他一開始(1985年)就把Chez開源會不會改變今天的IT格局呢? 哪位開發者穿越回去試試改變歷史吧.

$ a6osx/bin/schemenChez Scheme Version 9.5nCopyright 1984-2017 Cisco Systems, Inc.n

當然要嘗試中文標識符, 蠻好:

> (cons 火腿 (雞蛋))n(火腿 雞蛋)n> (define 階乘n (lambda (x)n (if (zero? x)n 1n (* x (階乘 (1- x))))))n> (階乘 3)n6n

發現一個小問題, 在控制台下, 在輸入後括弧時, 匹配前括弧的游標定位有錯位, 猜測是由於中文字元的寬度不同導致的. 在之後使用中, 發現對上一個命令進行編輯也有顯示問題. 這使得在交互環境中使用中文命名有了不小障礙(想想在上個程序基礎上任何一點修改都要重新輸入整個程序). 試著在源文件中編寫階乘函數後導入, 發現中文文件名也不支持(多謝 @Eternal Chaos 指出, 已有問題報告command-line-arguments cant read umlauts with utf-8 encoding · Issue #81 · cisco/ChezScheme), 不過導入成功.

看了一點書之後發現...好像裝了也不能直接用, 沒有那個J-Bob好像基本上跑不了什麼東西.

推薦閱讀：