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

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

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

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

(define 為空?
  (lambda (列表)
    (if (atom? 列表)
        'nil
        't)))

(define 相等?
  (lambda (甲 乙)
    (if (equal? 甲 乙)
      't
      'nil)))
 

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

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

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

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

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

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

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

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

舉例如下:

之前的定律car/cons

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

可以作用於下面表示式:

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

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

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

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

(為空? (car a))

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

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

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

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

$ a6osx/bin/scheme
Chez Scheme Version 9.5
Copyright 1984-2017 Cisco Systems, Inc.

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

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

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

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