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

圖靈百年之後,『計算』並沒有變得更『簡單』,『爆炸』般的『知識』也沒使得『邏輯』推演更加『清晰』。或許那台『仙女計算機』並沒有『使用手冊』?還是她有使用手冊,祇可惜缺少那個伴隨著通過『圖靈測試』之『演算法』的呢??

拉丁語 tertium non datur 聲稱︰

任何命題 P, \ (P \ \vee \sim P) 必真。

這個叫做『排中律』的概念,有直覺主義的數學家反對,後來還成立了一個『數學建構主義』的流派。這不就是句『空話』的嗎?又何必需要反對?原因在於並非所有的概念都是可以,像『真假』、『是非』與『對錯』般的『二分』,在『黑白』之外不只有『』,甚至還有『』。所以使用排中律一不小心就可能產生『虛假兩難論證』False dilemma。比方說有人論證想反駁『小三之歌』的『沒有拆不散的家庭,只有不努力的小三』︰

假使愛情堅定,無論如何考驗也不會改變;如果愛情不堅定,沒有小三也難長存。只有愛情堅定才會攜手建立家庭,所以再努力的小三也沒有用。

作者不知『堅不堅定』的兩極之間,果真該不該有『其他愛情』的存在?因此無法判斷這個論證對錯是否如此??而『直覺邏輯者』卻認為應該取消排中律︰

平面上任何一條不自相交連續之『封閉曲線C,將平面分成『』個區域,『C 之外或C 之內』之『二分』不包含著『C 之中』,但它不是才是 C 的啊!!

看來仙女早已遠離,那就說說存在的這台『圖靈機』吧!根據『 Hopcroft, John E.; Ullman, Jeffrey D. (1979). Introduction to Automata Theory, Languages, and Computation (1st ed.)』所定義︰

單磁帶』one-tape 圖靈機是一個有序七元組 M= \langle Q, \Gamma, b, \Sigma, \delta, q_0, F \rangle ,此處

Q 是一個有限非空的『狀態』 state 集合

\Gamma 是一個有限非空的『磁帶上字母符號』集合

b \in \Gamma 是一個『空白符號』,唯一允許在任意計算步驟中無限次出現在磁帶上的符號

\Sigma\subseteq\Gamma\setminus\{b\} 是不包含空白符號的『輸入符號』集合

q_0 \in Q 是『初始狀態

F \subseteq Q 是『最終狀態』或稱作『接受狀態』,一般可能有 q_{accept}, q_{reject},q_{HALT}

\delta: Q \setminus F \times \Gamma \rightarrow Q \times \Gamma \times \{L,R\} 是稱作『轉移函式』transition function,其中 L,R 代表『讀寫頭』之向『左,右』移動,還有的增加了『不移動』no shift 的擴張

220px-Maquina

300px-Turing_machine_2b

500px-State_diagram_3_state_busy_beaver_4_

220px-Lego_Turing_Machine

220px-Hopcroft-ullman-old

圖靈機 M 將以下面方式運行:

開 機的時候首先將輸入符號字串 \omega=\omega_0\omega_1\ldots\omega_{n-1} \in \Sigma^* 依序的從左到右填寫在磁帶之第 0, 1, \ldots , n-1 編號的格子上, 將所有其它格子保持空白 ── 即填以空白符 b ──。 然後 M 的讀寫頭指向第 0 號格子,此時 M 處於狀態 q_0。 機器開始執行指令,按照轉移函式 \delta 所描述的規則進行逐步計算。 比方如果當前機器的狀態是 q,讀寫頭所指的格子中的符號是 x, 假使 \delta(q,x) = (q', x', L), 那麼機器下一步將進入新的狀態 q', 且將讀寫頭所指的格子中的符號改寫為 x', 然後把讀寫頭向左移動一個格子。 設使在某一時刻,讀寫頭所指的是第 0 號格子, 然而根據轉移函式它的下一步又將繼續向左移,此時它停在原處不動,也就是說,讀寫頭永遠不會移出了磁帶的左方界限。 設若在某個時刻 M 根據轉移函式進入了某種最終狀態 q_{final}, 則它立刻停機並留下磁帶上的結果字串。由於轉移函式 \delta 是一個部分函式,換句話說對於某些 q,x, \ \delta(q,x) 可能沒有可用的轉移定義, 如果在執行中遇到這種情況,機器依設計約定也將立即 q_{HALT} 停機。

─── 《紙張、鉛筆和橡皮擦

 

今日正逢『四月之魚』 Poisson d’avril ,

恰宜介紹這個『深奧』的瑪利歐『通關符碼』︰

/mario

Racket implementation of MarioLANG

MarioLANG is a 2d programming language, must like BrainFuck but with an extra twist. It is also the name of the author of this implementation.

 

親自驗證『圖靈機』之本事也︰

MarioLANG

MarioLANG is a two-dimensional esoteric programming language made by User:Wh1teWolf, based on Super Mario. The source code’s layout is similar to a Super Mario world, however the programs written in MarioLANG look like a completely normal application when compiled. It is even Turing-complete! This language was inspired by RubE On Conveyor Belts.

There is no official interpreter for MarioLANG and neither is a detailed specification on the exact behavior of items and instructions. However, User:myname made an interpreter mostly based on his own interpretation of unclear behaviors in Ruby [1]. There is also an interpreter written in C++ by User:T.J.S.1 which, besides just interpreting it like a normal interpreter does, can also simulate the evaluation of the code in a graphical animation using ANSI colours in the terminal. It can be found here.

Commands

Source code is comprised of parts, items, and instructions.

Parts

The world is built up by four different pieces:

  • = : Ground. If Mario has no ground below his feet he falls until he lands on either ground or EOF.
  • | : Wall
  • #  : Elevator starting point (can be both the highest or the lowest point on the elevator, however this is where Mario jumps onto the elevator.)
  • " : Elevator ending (can not be right or left from the starting position)

Items

When Mario finds one of the following items he executes its corresponding command.

  • ) : Move memory pointer right
  • ( : Move memory pointer left
  • + : Add one to the memory cell under the pointer
  • - : Subtract one from the memory cell under the pointer
  • . : Output ascii character from current memory cell
  • : : Output numeric value from current memory cell
  • , : Input ascii character to current memory cell
  • ; : Input numeric value to current memory cell

Instructions to Mario

  • > : Go right
  • < : Go left
  • ^ : Jump
  • ! : Stop walking
  • [ : Skip next command if current memory cell is zero
  • @ : Start walking the other way

Anything not recognized as a command is a comment.

 

為何『改寫』

Examples

Commands Explained

++++:       >       >  +:+:+:+:+:+:+:::::
====+      >^===    """=================
    +:-):(:^=   =                       !
    =========    =                      #
                  = !             .+.,:-<
                   =###           ======"

Output: 4 60 5 6 7 8 9 10 11 12 12 12 12 12 11

 

耶?只求『結果』之一致ㄚ!

※ 註︰

那個 mario 似乎不會『跳』 ^;而且『電梯啟停』指令# 的『解釋』彷彿有懸疑ㄛ。

 

邱奇-圖靈論題

邱奇-圖靈論題英語:Church–Turing thesis,又稱邱奇-圖靈猜想邱奇論題邱奇猜想圖靈論題)是一個關於可計算性理論的假設。該假設論述了關於函數特性的,可有效計算的函數值(用更現代的表述來說–在算法上可計算的)。簡單來說,邱奇-圖靈論題認為「任何在算法上可計算的問題同樣可由圖靈機計算」。

20世紀上半葉,對可計算性進行公式化表示的嘗試有:

這三個理論在直覺上似乎是等價的–它們都定義了同一類函數。因此,計算機科學家和數學家們相信,可計算性的精確定義已經出現。邱奇-圖靈論題的非正式表述說:如果某個算法是可行的,那這個算法同樣可以被圖靈機,以及另外兩個理論所實現。

雖然這三個理論被證明是等價的,但是其中的前提假設–「能夠有效計算」是一個模糊的定義。因此,雖然這個假說已接近完全,但仍然不能由公式證明。

假說前提

已知的三種計算過程(遞歸λ演算圖靈機)都是等價的–這三種方法定義了同一類函數。這導致數學家和計算機科學家相信可計算性的概念可由上述三種等價的計算過程描述。簡單來講,邱奇-圖靈論題認為如果某種方法(算法)可進行運算,那麼該運算也可被圖靈機執行(也可被遞歸定義的函數或λ函數執行)。

邱奇-圖靈論題是對計算特性進行描述的一種陳述,故而不能被嚴格證明。雖然上面提到的三種計算過程可被證明為等價的,但是邱奇-圖靈論題最根本的前提–聲稱一個函數是「可有效計算的」究竟意味著什麼–在某種意義上是不甚明確的直覺結果。所以,該論題依然是一個假想。

儘管邱奇-圖靈論題不能被證明,到目前為止它仍然受到近乎全面的接受。

正式闡述

Rosser於1939年對「可有效計算性」進行了如下的解讀:「很明顯CC和RC(邱奇和Rosser的論據)的成立依賴於對『有效性』的嚴格定義。『有效的方法』主要是指該方法的每一步都可被事先確定,而且該方法可在有限的步數之內生成結果」。因此,『有效性』實際上包含兩層含義:

  1. 產生一種確定的,或者所需的效果
  2. 能夠產生計算結果

接下來, 術語「可有效演算的」意味著「由任何直觀上有效的方法產生的」,而術語「可有效計算的」意味著「由圖靈機或任何等價的機械設備產生的」。圖靈本人對此的定義由他在1939年的博士論文「基於有序數的邏輯系統」的腳註中給出:

我們應該使用『可計算函數』來表示一個可被機器計算的函數, 使用『可有效演算的』來指代那些並未特別指明的直觀想法。」

這可以轉述如下:

任何可有效演算的函數都是可計算函數。

圖靈則是如此描述的:

「當一個函數的值可由某種純機械計算步驟得到時, 它就是可有效演算的函數…應該這樣認識: 可計算性和可有效演算性是不同的。」

 

雖很重要,暫且放下☺