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

美國數學家阿隆佐‧邱奇 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.

220px-Euclid_flowchart_1

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

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

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

假使有兩個集合 ST,將之稱作『定義域』domain 與『對應域』codomain,函數 fS \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
>>>