樹莓派、樹莓派之學習、樹莓派之教育

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

2019-03-31 懸鉤子

假使說給定了一個『 λ表達式』 $(\lambda x. ((\lambda y. (x \ y)) \ \Box) \ \bigcirc)$ ，有人『第一步』這樣作『 $\beta$ 化約』︰

$((\lambda y. ( \bigcirc \ y)) \ \Box )$

，也有人『第一步』這樣作『 $\beta$ 化約』︰

$(\lambda x. ( (x \ \Box ) \ \bigcirc)$

，這樣不同的『步驟選擇』是否會產生『不同結果』的呢？如果說再次繼續進行『 $\beta$ 化約』，兩者都會得到︰

$(\bigcirc \ \Box )$

，於是我們就可以歸結的說『 $\beta$ 化約』不管是用著怎麽樣的『步驟次序』，都一定能夠得到『相同結果』的嗎？？

為了考察不同次序步驟的『化約策略』，首先讓我們定義『單步 $\beta$ 化約』︰

$A \equiv_{\beta^1} B$

是指表達式 $B$ 是經由表達式 $A$ 中的某一函式應用子表達式 $C =_{df} ((\lambda x. M) N)$ 『 $\beta$ 化約』而得來。假使『約定』零步 $\beta$ 化約是說『 $A \equiv_{\beta^0} A$ 』，這樣我們就可以說『單步』或『多次單步』之『單步 $\beta$ 化約』的『化約封閉性』︰

$U \equiv_{\beta^*} V$

，是講存在一個『單步 $\beta$ 化約』的『序列』

$U =_{df} S_1, S_2, S_3, \cdots, S_k, S_{k+1}, \cdots, S_n =_{df} V, \ S_k \equiv_{\beta^1} S_{k+1}, k=1\cdots n$

。某一表達式 $U$ 我們稱它是『 $\beta$ 可化約』 $\beta$ -redex 是指這個表達式還有『未化約』的子應用表達式 $((\lambda x. M) N)$ 。如果經過『有限的』化約序列，最終抵達一個『沒有未化約』的表達式 $V$ ，也就是說 $V$ 中沒有 $\beta$ -redex，這時我們將 $V$ 稱之為『 $\beta$ 正規元型』normal form。於是我們就可以問︰

各種不同的『化約序列』如果存在『 $\beta$ 正規元型』，那它們是相同的嗎？

【Church-Rosser 定理】說

如果 $P \equiv_{\beta^*} Q$ 而且 $P \equiv_{\beta^*} R$ ；那麼就會存在一個 $S$ ，使得 $Q \equiv_{\beta^*} S$ 以及 $R \equiv_{\beta^*} S$ 。

所以可以講不同的『化約序列』之『 $\beta$ 正規元型』，除了其內函式中的『受約束變元』之『虛名』不同外 ── 可以作『 $\alpha$ 變換』使之一樣 ──，都是『相同的』。這是一個非常重要的歸結，設想萬一它不是這樣，那所謂的『計算』不就成『笑話』了嗎！然而需要小心的是『 $\beta$ 化約』是『單行道』，也就是說 $A \equiv_{\beta} B$ 成立，並不代表 $B \equiv_{\beta} A$ 正確。比方講 $((\lambda x. x) a) \equiv_{\beta} a$ ，從結果變元 $a$ 又要怎麼得回原來函式應用的呢？

那麼『 $\beta$ 化約策略』Reduction Strategy 又是什麼呢？它是一個『函式』 $RS$ ，可以定義如下︰

一、『定義域』與『對應域』是『所有的 λ 表達式』構成的集合

二、如果 $e$ 是一個『 $\beta$ 正規元型』， $RS(e) = e$

三、假使 $m$ 不是『 $\beta$ 正規元型』，化約策略會依據特定方式選擇 $m$ 中的某一『優先』 $\beta$ -redex 子表達項 $t$ ， $RS(m) = t$

這樣看來 $RS$ 函式選擇了特定的『步驟次序』── 策略 ── 來作『單步 $\beta$ 化約』，這也是『程式』之『最佳化』optimize 的源起。然而不是每種『化約策略』都能夠抵達存在的『 $\beta$ 正規元型』。舉例說兩種簡單的『左』和『右』化約策略，它總是優先選擇表達式中的『最左』與『最右』 $\beta$ -redex 子表達項。

考慮用『左右』策略化約下面的表達式

$(((\lambda x. (\lambda y. x)) (\lambda z. z)) (\lambda w. (w w)))$

。

用『左』策略會得到『上圖』，用『右』策略會卡在 $(\lambda w. (w w))$ 。

所謂的『正規策略』是說用這個策略能夠得到『所有可能存在的』 $\beta$ 正規元型。事實上從邏輯推理可以證明『最左優先』策略是一種『正則策略』，果真是『天左旋』的乎！！

最後讓我們談談『相等』的概念以及『等號 $=$ 』的使用，相等和『邏輯推導規則』有關︰

一、 $\frac{}{X = X}$ ，無條件自反律

二、 $\frac{X = Y}{Y = X}$ ，對稱律

三、 $\frac{X = Y \wedge Y = Z}{X = Z}$ ，遷移律

此處的 $\frac{Premises}{Conclusion}$ 是講，如果由『前提』Premises，我們可以邏輯上推導出『結論』Conclusion。也就是說這是廣義的『相等』關係的『內涵』。

此處雖然並不定義『 λ 運算』中所謂的『等式』到底是指什麼？只是從『基元』觀點下，就是說假設我們基本『知道』或者『同意』兩個表達式『 $A = B$ 』所指的意義── 比方說指相同的計算結果 ──，於是我們可以提出下面的『 λ 理論』︰

一、 $\frac{M = N}{(A M) = (A N)}$ ，『應用』於『等式』之『結果』相等

二、 $\frac{M = N}{(M A) = (N A)}$ ，『等式』之『函式』的『應用』相等

三、 $\frac{M = N}{(\lambda x. M) = (\lambda x.N)}$ ，『等式』之『函式抽象』相等

四、 $\frac{}{((\lambda x. M) A) = M[x := A]}$ ，『應用』是無條件的『化約相等』

五、 $\eta$ 擴張， $\frac{}{(\lambda x. (M x)) = M}$ ，『外延』相同的『函式』相等

簡單的將『變元』、『函式』和『應用』結構起來形成的『 λ 運算』，彷彿是『概念』的『水滴』墜落『心湖』，激起『思想』的『浪花』。這些『浪花』彼此『碰撞』，掀起陣陣『漣漪』，最後『波光』點點，早就分不清哪兒是『始點』，哪兒又是『終點』！！

─── 《Λ 運算︰概念導引《四》》

知道 $\lambda - redex$ 是什麼。且能將之聯繫上 PLT

Programming language theory

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting mathematics, software engineering, linguistics and even cognitive science. It is a well-recognized branch of computer science, and an active research area, with results published in numerous journals dedicated to PLT, as well as in general computer science and engineering publications.

History

In some ways, the history of programming language theory predates even the development of programming languages themselves. The lambda calculus, developed by Alonzo Church and Stephen Cole Kleene in the 1930s, is considered by some to be the world’s first programming language, even though it was intended to model computation rather than being a means for programmers to describe algorithms to a computer system. Many modern functional programming languages have been described as providing a “thin veneer” over the lambda calculus,^[1] and many are easily described in terms of it.

The first programming language to be invented was Plankalkül, which was designed by Konrad Zuse in the 1940s, but not publicly known until 1972 (and not implemented until 1998). The first widely known and successful high-level programming language was Fortran, developed from 1954 to 1957 by a team of IBM researchers led by John Backus. The success of FORTRAN led to the formation of a committee of scientists to develop a “universal” computer language; the result of their effort was ALGOL 58. Separately, John McCarthy of MIT developed the Lisp programming language (based on the lambda calculus), the first language with origins in academia to be successful. With the success of these initial efforts, programming languages became an active topic of research in the 1960s and beyond.

大體明白 PLT Redex 名目也︰

Welcome

PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics.

PLT Redex is embedded in Racket, meaning all of the convenience of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.

Getting started: Install Racket, and try the tutorial.

Book: Semantics Engineering with PLT Redex (SEwPR) by Matthias Felleisen,Robert Bruce Findler, and Matthew Flatt gives the mathematical background for operational semantics, as well as a tutorial introduction to Redex. The preface, table of contents, and an example syllabus are available online. The book is available fromMIT Press.

Documentation: The reference manual contains all of the gory details of all of Redex’s operators.

Citation: If you use a reduction semantics and/or you modeled a reduction semantics with Redex and you wish to give academic credit, please cite the book (above). If you are studying the effectiveness of meta-tools, the proper citation is our POPL 2012 paper.

至於那個

v.7.2

2 Long Tutorial

This tutorial is derived from a week-long Redex summer school, run July 27–31, 2015 at the University of Utah.

2.1 The Theoretical Framework

Goals

— abstract syntax

— notions of reduction, substitution

— reductions and calculations

— semantics

— standard reduction

— abstract register machines

— types

The lambda calculus:

e = x | (\x.e) | (e e)

Terms vs trees, abstract over concrete syntax

Encode some forms of primitives: numbers, booleans – good for theory of computation; mostly irrelevant for PL. extensions with primitive data

e = x | (\x.e) | (e e) | tt | ff | (if e e e)

What we want: develop LC as a model of a PL. Because of history, this means two things: a simple logic for calculating with the terms of the language e == e’ and a system for determining the value of a program. The former is the calculus, the latter is thesemantics.

Both start with basic notions of reduction (axioms). They are just relation on terms:

((\x.e) e’) beta e[x=e’]

pronounced: e with x replaced by e’

((\x.e) e’) beta [e’/x]e

pronounced substitute e’ for x in e

Think substitution via tree surgery, preserving bindings

Here are two more, often done via external interpretation functions (δ)

(if tt e e’) if-tt e

(if ff e e’) if-ff e’

If this is supposed to be a theory of functions (and if expressions) we need to be able to use this relations in context

e xyz e’

————–

e = e’

e = e’ e = e’ e = e’

————– ————– ————–

e e” = e’ e” e” e = e” e’ \x.e = \x.e’

plus reflexivity, symmetry, and transitivity

for any relation xyz

Now you have an equational system. what’s it good for? you can prove such facts as

e (Y e) = (Y e)

meaning every single term has a fixpoint

All of the above is mathematics but it is just that, mathematics. It might be considered theory of computation, but it is not theory of programming languages. But we can use these ideas to create a theory of programming languages. Plotkin’s 1974 TCS paper on call-by-name versus call-by-value shows how to create a theory of programming languages.

In addition, Plotkin’s paper also sketches several research programs, mostly on scaling up his ideas to the full spectrum of languages but also on the precise connection between by-value and by-name their relationship, both at the proof-theoretical level as well as at the model-theoretic level.

Here is Plotkin’s idea as a quasi-algorithm:

Start from an abstract syntax, plus notions of scope and scope-preserving substitution. Consider closed terms Programs.
Identify a subset of expressions as Values. Use v to range over Values.Note The complement of this set was (later) dubbed computations, due to Moggi’s work under Plotkin.
Define basic notions of reduction (axioms). Examples:

((\x.e) e’) beta-name e[x=e’]

((\x.e) v) beta-value e[x=v]
Inductively generate an equational theory from the basic notions of reduction.
This theory defines a semantics, that is, a relation eval from programs to values:

eval : Program x Value

def e eval v iff e = v
Prove that eval is a function, and you have got yourself a specification of an interpreter.

eval : Program -> Value

eval(e) = v

Note This step often reuses a variant of the Church-Rosser theorem of the mathematical theory of lambda calculus.
Prove that the calculus satisfies a Curry-Feys standard reduction property. This gives you a second semantics:

eval-standard : Program -> Value

def eval-standard(e) = v iff e standard reduces to v

The new semantics is correct:

Theorem eval-standard = eval

Standard reduction is a strategy for the lambda calculus, that is, a function that picks the next reducible expression (called redex) to reduce. Plotkin specifically uses the leftmost-outermost strategy but others may work, too.

Plotkin also shows—on an ad hoc basis—that this evaluator function is equivalent to Landin’s evaluator based on the SECD machine, an abstract register machine.

Plotkin (following Morris, 1968) uses step 6 from above to add two ideas:

The interpreter of a programming language (non-constructively) generates a theory of equivalence on phrases.

def e ~ e’ iff placing e and e’ into any context yields programs that produce the same observable behavior according to eval

Theorem ~ is the coarsest equivalence theory and thus unique.

Let’s call ~ the Truth.
Theorem e = e’ implies e ~ e’. Naturally the reverse doesn’t hold.

Matthias’s (post)dissertation research extends Plotkin’s work in two directions:

Plotkin’s “algorithm” applies to imperative programming language, especially those extending the lambda calculus syntax with (variable) assignment and non-local control operators.Imperative Extensions explains how two of these work.
It is possible to derive useful abstract register machines from the standard reduction semantics of the programming language
Each machine M defines a new semantics:

def eval-M(e) = v iff load M with e, run, unload, yields v

For each of these functions, we can prove an equivalence theorem.

Theorem eval-M = eval-standard = eval

His work also shows how this approach greatly simplifies proofs of consistency for the semantics of programming languages and especially so-called type soundness theorems.

未曾深研，不敢亂講呦。

樹莓派、樹莓派之學習、樹莓派之教育

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

2019-03-30 懸鉤子

${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.

………

語義園地也。

樹莓派、樹莓派之學習、樹莓派之教育

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

2019-03-29 懸鉤子

古來就有『晨星』『暮星』之惑；當日太白金星之為天神。又以朝見於東謂之『啟明』，夕位於西而曰『太白』，主殺伐。此事故東西皆然，祇可抱之以微笑 Smile 了！！

由於人們對於語言文字習以為常，以至於論述時其『所指』到底『存在』或是『不存在』反而不甚了了了。比方說吧

白色的念頭躺在茵茵的草地上

，這句話要作何解釋？如果用下面的議論可以嗎？

白色的念頭在我的腦海裡，我躺在茵茵的草地上之故

。西方中世紀的繁瑣哲學能夠論證『一根針尖上有多少個天使在跳舞』，這能相信嗎？？繼《概念文字》一書之後，於一八九二年弗雷格發表了兩篇重要的論文《論概念和對象》與《論意義和指稱》，開了『符號學』的大門，深入『語意學』的廳堂，將分析哲學推向另一座高峰。那這門學問到底說些什麼呢？比方說『馬』這個字吧︰一、馬字是個象形的符號；二、它是像著自然中可見的『那種動物 』── 馬是什麼？這構成了馬的『概念』，它可用以分辨『異同於馬』之物 ──；三、那種動物就是馬的『指稱』；四、這個指稱成為馬字代表的『意義』。當人們有了很多自然的、社會的『事事物物』的概念之後，或許『忘了』符號總是『抽象的』，不同於它所代表的存在之事物，更不要說事物可能進化變遷，而符號也會在世代間存有差異。就像『獨角獸』一詞所說的那種獸果真存在嗎？一定不存在嗎？如果有一隻『獨角牛』，那它是『獨角獸』嗎？假使將來發現一種『獨角馬』，那它也是『獨角獸』嗎？其次符號與符號的用法是『兩回事』，有人是否『意有別指』，特不加以區分故說著︰『戰爭』一點也不可怕，它只是『兩個字』！！再者，抽象的概念又可能會發生『自我指涉』的情況，舉例說︰

框框裡的這句話是『假的』。

，它自己說自己是假話，真是假作真時真亦假！！因此當用『集合論』時，這個

{ x | P x}

所說的 ── 所有擁有『 P 屬性』的這種東西構成一個集合 ──這個集合是否會矛盾呢？會不會是個什麼都沒有『 ∅ 』空集合呢？這就需要小心的了。其實悖論還常常能有『大用』，建構彼此互相『矛盾』的命題，揭示『不相容』於『已證明』的事物，這就是所謂的『歸謬證法』，比方說幾何學之父的歐幾里得 ── 或許是師法畢達哥拉斯 ──的 $\sqrt {2}$ 是無理數的證明︰
假設 $\sqrt {2}$ 是有理數，可以寫成無公因數的最簡分數 P/Q，也就是 $\sqrt {2}$ = P/Q 。
所以，2‧ $Q^2$ = $P^2$ ，這樣 P 就一定是『偶數』，就說 P = 2‧S 吧，將它代入上式，得到
$Q^2$ = 2‧ $S^2$ ，這樣 Q 也一定是『偶數』，
於是和『假設』矛盾，證明了『結論』。

─── 《{X|X ∉ X} ！！？？》

於是我們可以說︰ PyonR 之語義及語境與 Python 2.7 並不『對等』 equivalent 。就像『…』的解釋實有『差異』也︰

rock64@rock64:~ cd lambda-py/base/
rock64@rock64:~/lambda-py/base cat test.py |racket python-main.rkt --interp
已砍掉
rock64@rock64:~/lambda-py/base echo "print('lambda-py works')" | racket python-main.rkt --interp
lambda-py works

陷入沉思哩！

因此先試著深入了解美麗球拍呦☺

Beautiful Racket / tutorials

Our stacker language maintains a stack of arguments, which starts out empty. Each line of the program represents a new argument for the stack. If it’s a number, it’s simply pushed onto the top of the stack. But if it’s an operator—either + or *—then the top two arguments from the stack are popped off, and replaced with the result of applying the operator (meaningarg1 + arg2 or arg1 * arg2). So the sample program above means3 * (8 + 4), and when it runs, the result is 36.

…

……

Enlarge the solution space. It doesn’t matter which language you like best or use most—sometimes you encounter a problem that doesn’t mesh with the language idiom. When you make a language, you expand your possibilities, which also allows the solution to be carefully tailored to the problem.
Certain programs naturally describe languages. Languages are good for what we might call wide-funnel problems, where there’s a large universe of possible inputs, but a relatively small scope of outputs. (How to tell: does your program take input from arbitrarily complex files, and turn them into a simpler representation?)
Better glue. A little language can fill holes in a larger toolchain. For instance, Python doesn’t have a preprocessor like C does, but you could make one as a DSL. (Python fans, please don’t write me to explain why this is a bad idea. I’m not here to say what you should do, just what you can do.)
Better interface. Whether you work alone or in a team, a language can wrap a streamlined, easy-to-understand interface around other code.
You’ll know something others don’t. Knowing how to make a programming language will teach you ideas that you can fold into your usual programming work.

………

Design the notation and behavior of our new language.
Write a Racket program that takes source code written in the new language and converts its notation and behavior to an equivalent Racket program.
Run this new Racket program normally.

樹莓派、樹莓派之學習、樹莓派之教育

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

2019-03-28 懸鉤子

美國數學家阿隆佐‧邱奇 Alonzo Church 對『符號邏輯』symbolic logic 的熱情與對基礎算術『形式系統』的研究持續一生。當他發現這類系統容易受到『羅素悖論』影響時，轉將所設想的『λ 運算』lambda calculus 單獨用於研究『可計算性』問題，同樣否定的回答了『判定性問題』 Decision-problem ──

一九零零年德國大數學家大衛‧希爾伯特 David Hilbert 在巴黎的國際數學家大會上作了場名為《數學問題》的演講，提出了二十三道待解決之最重要的數學問題，這就是著名的希爾伯特之二十三個問題的由來。這裡的『判定性問題』就是二十三個問題的第二題『算術公理之相容性』，一九三零年已為庫爾特‧哥德爾所否證 ──。美國 UCLA 大學 Enderton, Herbert B. 教授寫了一篇名為
《INTRODUCTION
Alonzo Church: Life and Work》的 Alonzo Church 小傳︰
…
In 1936 a pair of papers by Church changed the course of logic. An Unsolvable Problem of Elementary Number Theory presents a definition and a theorem:
“The purpose of the present paper is to propose a definition of effective calculability which is thought to correspond satisfactorily to the somewhat vague intuitive notion . . . , and to show, by means of an example, that not every problem of this class is solvable.” The “definition” now goes by the name Church’s Thesis: “We now define the notion . . . of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a λ-definable function of positive integers).” (The name, “Church’s Thesis,” was introduced by Kleene.)
The theorem in the paper is that there is a set that can be defined in the language of elementary number theory (viz. the set of G ̈odel numbers of formulas of the λ-calculus having a normal form) that is not recursive—although it is recursively enumerable. Thus truth in elementary number theory is an effectively unsolvable problem.

A sentence at the end of the paper adds the consequence that if the system of Principia Mathematica is ω-consistent, then its decision problem is unsolvable. It also follows that the system (if ω-consistent) is incomplete, but of course G ̈odel had shown that in 1931.
…

λ演算是一套用來研究『函式』Function 的『抽象』Abstraction 、函式的『應用』Apply 、『變元』Variable 的『替換』Substitution 以及『函式』之『化約』reduction 的形式語言。λ演算對於泛函式程式語言的興起有著巨大的推動力，比方說人工智慧領域著名的 Lisp 語言，以及後來的 ML 語言和 Haskell 語言。更令人驚訝的是它自身就是一個『世界上最小的通用性程式語言』。由於『函式』與『變元』兩者是任何人不管想用哪種『□□程式語言』來寫『演算法』Algorithm 都需要清楚理解的概念。就讓我們踏上前人走過的足跡，回顧旅途上周遭景緻，說不定會有意外的收穫！！

首先請讀者參考在《Thue 之改寫系統《一》》一文中的『符號定義』，於此我們引用該文中談到數學裡『函數定義』的一小段︰

如此當數學家說『函數』 $f$ 的定義時︰

假使有兩個集合 $S$ 和 $T$ ，將之稱作『定義域』domain 與『對應域』codomain，函數 $f$ 是 $S \times T$ 的子集，並且滿足

$\forall x \ x \in S \ \exists ! \ y \ y \in T \ \wedge \ (x,y) \in f$

，記作 $x \mapsto y = f (x)$ ，『 $\exists \ !$ 』是指『恰有一個』，就一點都不奇怪了吧。同樣『二元運算』假使『簡記』成 $X \times Y \mapsto_{\bigoplus} \ Z$ ， $X=Y=Z=S$ ，是講︰

$z = \bigoplus ( x, y) = x \bigoplus y$ ，也是很清晰明白的呀！！

─── 《Λ 運算︰淵源介紹》

如何回答

$Python(CPython) \ \frac{?}{\equiv} \ PyonR(Racket)$

是否『同義』之大哉問呢？

假使任一 Python 2.7 的『原始碼』以 PyonR 『解讀』的『結果』都『一樣』，能不能『同意』也！

如果不只走馬看花︰

應探索其限制︰

Use:

To use PyonR with DrRacket, simply replace #lang racket with #lang python.

Limitations:

PyonR currently supports most of the Python language as specified by version 2.7, except for a few constructs (most notably thedel and with statements, decorators and the super function for constructors) and some missing methods on built-in types.

rock64@rock64:~$ python
Python 2.7.13 (default, Sep 26 2018, 18:42:22) 
[GCC 6.3.0 20170516] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> def f():
...    return f.x
... 
>>> f.x = -1
>>> f()
-1
>>>

當思『實用性』不足為斷ㄚ◎

Python 2.7.13 (default, Sep 26 2018, 18:42:22) 
[GCC 6.3.0 20170516] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> def counter():
...     counter.count += 1
...     return counter.count
... 
>>> counter.count = 5
>>> counter()
6
>>> counter()
7
>>> counter()
8
>>>

樹莓派、樹莓派之學習、樹莓派之教育

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

2019-03-27 懸鉤子

初步通讀

v.7.2

The Racket Guide

Matthew Flatt,
Robert Bruce Findler,
and PLT

This guide is intended for programmers who are new to Racket or new to some part of Racket. It assumes programming experience, so if you are new to programming, consider instead reading How to Design Programs. If you want an especially quick introduction to Racket, start with Quick: An Introduction to Racket with Pictures.

Chapter 2 provides a brief introduction to Racket. From Chapter 3 on, this guide dives into details—covering much of the Racket toolbox, but leaving precise details to The Racket Reference and other reference manuals.

…

略為了解

v.7.2

DrRacket: The Racket Programming Environment

Robert Bruce Findler
and PLT

DrRacket is a graphical environment for developing programs using the Racket programming languages.

……

忽爾在

Racket Packages

These are the packages in the official package catalog.

raco pkg install package-name installs a package.

………

裡，發現這個套件

python

pedropramos@tecnico.ulisboa.pt

An implementation of the Python programming language for Racket

This package needs documentation

Tags:

language

眼精斗然一亮☆

谷歌才知道，原來是篇論文

內容十分豐富，況自許先鋒哩！

pedropramos/PyonR

A Python implementation for Racket

PyonR

PyonR (pronounced “Pioneer”) is an implementation of the Python programming language for the Racket platform.

焉能不嚐鮮呦？

FreeSandal

每月彙整: 2019 年 3 月

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

Programming language theory

History

2 Long Tutorial

2.1 The Theoretical Framework

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

Redex: Practical Semantics Engineering

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

Beautiful Racket / tutorials

What is a programming language?

Why should I make a programming language?

How are languages implemented in Racket?

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

Use:

Limitations:

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

The Racket Guide

DrRacket: The Racket Programming Environment

Racket Packages

python

pedropramos/PyonR

PyonR

輕。鬆。學。部落客

History

2 Long Tutorial

2.1 The Theoretical Framework

Beau­ti­ful Racket / tuto­ri­als

Limitations:

pedropramos/PyonR

PyonR

輕。鬆。學。部落客

Beautiful Racket / tutorials