Rock It 《ML》JupyterLab 【丁】Code《七》語義【六】解讀‧四‧Redex 一

${1\over 2} < \left\lfloor \mathrm{mod}\left(\left\lfloor {y \over 17} \right\rfloor 2^{-17 \lfloor x \rfloor - \mathrm{mod}(\lfloor y\rfloor, 17)},2\right)\right\rfloor$

二零零一年加拿大傑夫‧塔珀 Jeff Tupper 所發現的自指公式，它的二維『函數圖像』，與數學的『公式外觀』相仿。

一九二九年比利時畫家雷內‧弗朗索瓦‧吉蘭‧馬格利特 René François Ghislain Magritte 名作《形象的叛逆》The Treachery of Images 上用法文寫著『你看到的不是煙斗』。

一九零四年荷蘭著名品牌德羅斯特 Droste 所販售的可可粉之包裝盒上的圖片是一位護士拿著一個上有杯子及紙盒的托盤，托盤裡的杯子和紙盒上之圖案也就是這張圖片。

不過『自我指涉』可能會產生『矛盾』，『遞迴』也許將陷入『無窮循環』，然而它們的『魅力』卻是歷久彌新！！

『抽象』的概念雖然『無象』可以用來作『想象』，就如同前面談到過的『思想實驗』一樣，還是可以建造『情境』方便『觀相』的。假使說『思考』是根『概念磁鐵』，那麼『思維』就是『磁力線』。從『創造發想』的『發散處』出發，抵達『清晰自恰』之『收斂點』。因此『磁力線』的『封閉性』也可比喻成『思維』是『自我遞迴』的了。這樣或許『思考』在『博』與『精』的方面能夠成為『自行車』之『雙輪』，而這個『操控』之人也逐漸地步上了『收發自如』的道路。

讓我們再次思考邱奇自然數的構造

$n =_{df} \lambda f. \lambda x. \ f^n \ x$
$\equiv \lambda f. \lambda x. \ f(\cdots(f x))$
$\equiv \lambda f. \lambda x. \ f(f^{n-2}(f x))$

，這說明了變元 $f, x$ 在結構中的位置，以及『應用求值策略』也許是『外到內』 $f [f^{n-1} x]$ 或者是『內到外』 $f^{n-1}(f x)$ 。當我們在『解讀』一個表達式時，什麼將會是『變元』 $f, x$ 的『賦值』，以及它們的『性質』，往往就是『理解』表達式的『關鍵處』，以及自己『構思』的『起始點』。舉個『ISZERO』例子說

$ISZERO =_{df} \lambda n. n (\lambda x. \ FALSE) \ TRUE$

$ISZERO \ n$
$\equiv_{\beta} n \ (\lambda x. \ FALSE) \ TRUE$
$\equiv_{\beta} (\lambda f. \lambda x. \ f^n \ x) \ (\lambda x. \ FALSE) \ TRUE$
$\equiv_{\beta} {(\lambda x. \ FALSE)}^{n-1} (\lambda x. \ FALSE \ TRUE)$
$\equiv_{\beta} (\lambda x. \ FALSE) \ {(\lambda x. \ FALSE)}^{n-1} (TRUE)$

，然而 $((\lambda \bigcirc. \ FALSE) \ \Box) \equiv_{\beta} FALSE, \ n \geq1$ ，這就是為什麼選擇『 $(\lambda x. \ FALSE)$ 』函式的原因。現在只剩下『0』的情況需要考慮了

$ISZERO \ 0$
$\equiv_{\beta} 0 \ (\lambda x. \ FALSE) \ TRUE$
$\equiv_{\beta} (\lambda f. \lambda x. \ x) \ (\lambda x. \ FALSE) \ TRUE$
$\equiv_{\beta} (\lambda x. \ x) \ TRUE$
$\equiv_{\beta} TRUE$

，所以也就是會用『TRUE』的理由。

在數學上既然有『加法』也就有『減法』，那麼能不能仿造 $n$ 的『後繼數』是 $n+1$ ，定義一個『前導數』predecessesor $n-1$ 的呢？也就是說在 $n$ 中想辦法『去掉一個 $f$ 』，下面的這個

$PRED =_{df} \lambda n. \lambda f. \lambda x. \ n \ (\lambda g. \lambda h. \ h \ (g \ f)) (\lambda u. x) \ (\lambda u. u)$

就是一個精巧的設計。

……

既然談『λ 運算』表達式，如果不講『遞迴』函式；就彷彿是人到了『巴黎』，卻又沒見着『艾菲爾鐵塔』。之前在《自我再現》中提到函數 $f$ 之『定點』的定義是 $x = f(x)$ ，此時 $x = f^n(x)$ 。然而『 λ 表達式』無法『直接』的『自我指涉』。有人問為什麼呢？回顧一下它的『定義』，每一個寫出來的表達式都是『匿名的』，如果連『名字』都沒有，又怎麼能夠『指涉其名』的呢？所以只能『迂迴』的『間接』透過其它函式來『指涉』所說的就是那個『匿名的□□』。就像『自我應用』組合子，在函式應用時，可以產生『自我作用』一樣。著名的哈斯凱爾‧卡瑞 Haskell Brooks Curry ── 組合邏輯的發展者，Haskell 與 Brooks 程式語言都用他的名字來命名 ──，發現了『 $Y$ 』組合子，現今稱作『Curry 之悖論組合子』。為什麼要叫做『悖論』的呢？因為『自我指涉』恐怕會產生『羅素悖論』之故！但是『 $Y$ 組合子』雖可能會『陷入』無窮推導，卻沒有『矛盾』，它的一個特性，就是使用『 λ 表達式』做『遞迴的關鍵』︰

$(Y \ g) \equiv_{\beta} (g \ ( Y \ g))$

，比對『定點』的定義，就可以知道函式應用 $(Y \ g)$ 是變元函式 $g$ 的『定點函式』，也就是說『藉著 $Y$ 』，將一個命名的變元函式 $g$ 轉成了『自我調用』。為了避免 $g$ 的『無窮推導』，就像數學裡『迴歸定義』一樣，總要有一個『中止條件』。假使

$r =_{df} \lambda f. \lambda n. IFTHENELSE \ (ISZERO \ n) \ (n_0) \ (\bigotimes n \ (f \ ( PRED \ n)))$

，如果定義的自然數二元運算 $\bigotimes$ 類似具有『加法』或『乘法』的性質， $r \ (Y \ r) \ n$ 的結果就是

$\bigotimes \ n \bigotimes (n-1) \cdots \bigotimes \ 1 \ n_0$

，這個 $r$ 就是使用『 λ 表達式』寫作『遞迴函式』的一般範例，而 $n_0$ 就是『中止條件』的化約『傳回值』。

─── 《Λ 運算︰計物數《下》》

承上篇，沉思 lambda-py 結果！

rock64@rock64:~ cat test.py 
l = []
l.append(l)
print(l)

rock64@rock64:~/lambda-py/base 
rock64@rock64:~/lambda-py/base cd lambda-py/base/
rock64@rock64:~/lambda-py/base cat test.py |racket python-main.rkt --interp
[[]]

那麼『…』

rock64@rock64:~ python3
Python 3.5.3 (default, Sep 27 2018, 17:25:39) 
[GCC 6.3.0 20170516] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> 無限大 = int('inf')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: invalid literal for int() with base 10: 'inf'
>>> 無限大 = float('inf')
>>> 無限大 == 無限大
True
>>> 無限大 * 0
nan
>>> nan = int('nan')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ValueError: invalid literal for int() with base 10: 'nan'
>>> nan = float('nan')
>>> nan == nan
False
>>> nan * 0
nan
>>> nan / nan
nan
>>> ... == nan
False
>>> ... == 無限大
False
>>>

踏入

v.7.2

Redex: Practical Semantics Engineering

Robert Bruce Findler,
Casey Klein,
Burke Fetscher,
and Matthias Felleisen

PLT Redex consists of a domain-specific language for specifying reduction semantics, plus a suite of tools for working with the semantics.

This manual consists of four parts: a short tutorial introduction, a long tutorial introduction, a reference manual for Redex, and a description of the Redex automated testing benchmark suite. Also see http://redex.racket-lang.org/ and the examplessubdirectory in the redex collection.

………

語義園地也。

日	一	二	三	四	五	六
« 4 月
			1	2	3	4
5	6	7	8	9	10	11
12	13	14	15	16	17	18
19	20	21	22	23	24	25
26	27	28	29	30	31

FreeSandal

Rock It 《ML》JupyterLab 【丁】Code《七》語義【六】解讀‧四‧Redex 一

Redex: Practical Semantics Engineering

輕。鬆。學。部落客