美國數學家阿隆佐‧邱奇 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 之改寫系統《一》》一文中的『符號定義』,於此我們引用該文中談到數學裡『函數定義』的一小段︰
如此當數學家說『函數』 的定義時︰
假使有兩個集合 和 ,將之稱作『定義域』domain 與『對應域』codomain,函數 是 的子集,並且滿足
,記作 ,『 』是指『恰有一個』,就一點都不奇怪了吧。同樣『二元運算』假使『簡記』成 ,,是講︰
,也是很清晰明白的呀!!
─── 《Λ 運算︰淵源介紹》
如何回答
是否『同義』之大哉問呢?
假使任一 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 >>>