人類的思維如果一旦不『審慎』，很容易邏輯『混亂』，以至於言論多所『謬誤』，有時或許『巧說詭辯』。比方說公孫龍子的『雞三足』之詭論︰…牛羊有毛，雞有羽。謂雞足一，數足二；二而一，故三。謂牛羊足一，數足四；四而一，故五。羊牛足五，雞足三，故曰：『牛合羊非雞』。非，有以非雞也。…裡頭的『謂雞足一』之『雞足』和『一』是什麼？『數足二』的『足』與『二』又是什麼？卻能相加，彷彿『一雞 + 二足』可以得到『三 』的一般？！已經完全不像他的『白馬非馬論』了。

洛基的賭注 Loki’s Wager
洛基乃北歐神話中以『詐騙』著名之神。傳說他曾與矮人打賭卻輸了。當矮人們依約來『提頭』時，洛基說︰『沒問題』，但是必須依照『約定』，只能取走『他的頭』，而不能動著『他的脖子』。於是彼此開始『爭論』該如何的『切割』：有哪些部分雙方同意『是頭』；又有哪些部分認同『是脖子』。只是脖子的『結束點』和頭之『開始點』究竟『是哪裡』，互相一直無法『取得共識』。於是洛基終於保住著了他的頭。

因此『語言學家』在『定義』他們的『術語』時，通常採取數學家和邏輯學家的『方式』，舉例說，集合 代表一個『形式語言』中的『字彙』集合，也就是說 的元素是某種『抽象』語言的語詞。假使 ，『序連』 concatenation 是指像『』這樣的把語詞串接成『字串』，那麼要如何表達『任意多個字彙序連的字串論域 』呢？他們使用著美國數學家 Stephen Cole Kleene 的『Kleene star』Kleene之星遞迴的表示成︰

，『空字串』的集合，
，
，
…
。

雖然這樣作有點『麻煩』，作的好處就是『清晰可驗證』。此處的『 』是包含零的『自然數系』，而『 』是不包含零的自然數系，假使所指的論域不包含空字串，一般會記成︰

。

比方英國的哲學家  Antony Garrard Newton Flew 於 1975 年在一本名為『 Thinking About Thinking:  Do I sincerely want to be right? 』書中講到︰

【沒有真正的蘇格蘭人 No true Scotsman】

想像一位名叫 Hamish McDonald 的蘇格蘭人，坐下打開他的《格拉斯哥先驅晨報》，看見一則新聞『布萊頓 ── 位於英格蘭南部 ──色魔再度犯案！』他震驚地說：『沒有蘇格蘭人會 幹這種事！』隔天他又打開報紙，看見新聞描述一位亞伯丁人 ── 該城位於蘇格蘭 ── 更殘暴的行為，相較之下布萊頓色魔還算是個紳士。這顯示 Hamish 的想法是 錯的，但他會承認嗎？似乎不會。這次他說：『沒有【真正的】蘇格蘭人會作這種事。』

今天這稱之為『訴諸純正』appeal to purity 的謬誤，是指在原先的普遍性宣稱遭遇反例時，隨即提出一個更『理想』的『標準』作為他辯護之依據。大概沒人知道這個 { □ |  □是純正蘇格蘭人} 到底有哪些元素？難到它不會是個   嗎？？

就讓我們『正式的』formal  將『 Thue 改寫系統』定義如下︰

semi-Thue 改寫系統是一個有序元組 ( , )，其中 是一個有限的『字母』alphabet 集合，它之Kleene之星是   ，包含空字串、有限字串或稱作字詞。 是一個建構於   的二元關係，也就是說 。每一個 中的元素 叫做一個『改寫規則』rewriting  rule，通常寫成 。假使關係 具有『對稱性』，這個系統便稱作『Thue 改寫系統』。

─── 《THUE 之改寫系統《二》》

回想起有人寫了個

nickodell/mlc

MarioLANG Compiler

MarioLANG Compiler

MarioLANG Compiler (mlc) will compile programs from MarioLANG into C.

Usage

 gcc ml.c
 cat example.ml 
++++:       >       >  +:+:+:+:+:+:+:::::
====+      >^===    """=================
    +:-):(:^=   =                       !
    =========    =                      #
                  = !             .+.,:-<
                   =###           ======"
rock64@rock64:~/mlc ./a.out 
4 6 0 5 6 7 8 9 10 11 12 12 12 12 12 11 h
hirock64@rock64:~/mlc

能將

MarioLANG → FSM ！

那麼這是可能的嗎？

Finite-state machine

Classes of automata

A finite-state machine (FSM) or finite-state automaton (FSA, plural: automata), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some external inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the conditions for each transition. Finite state machines are of two types – deterministic finite state machines and non-deterministic finite state machines.^[1] A deterministic finite-state machine can be constructed equivalent to any non-deterministic one.

The behavior of state machines can be observed in many devices in modern society that perform a predetermined sequence of actions depending on a sequence of events with which they are presented. Simple examples are vending machines, which dispense products when the proper combination of coins is deposited, elevators, whose sequence of stops is determined by the floors requested by riders, traffic lights, which change sequence when cars are waiting, and combination locks, which require the input of combination numbers in the proper order.

The finite state machine has less computational power than some other models of computation such as the Turing machine.^[2] The computational power distinction means there are computational tasks that a Turing machine can do but a FSM cannot. This is because a FSM’s memory is limited by the number of states it has. FSMs are studied in the more general field of automata theory.

不過有限行 MarioLANG 『程式』，可有無窮多『狀態』嗎？？

恐論理嚴謹無趣！！

故想求之以『真理機器』矣☆

The Truth Machine

The Truth Machine (1996) is a science fiction novel by James L. Halperin about a genius who invents an infallible lie detector. Soon, every citizen must pass a thorough test under a Truth Machine to get a job or receive any sort of license. Eventually, people begin wearing them all the time, thus eliminating dishonesty in all parts of human interaction, and eliminating crime, terrorism and a great deal of general social problems.

Plot

The novel primarily focuses on the life story of Randall Peterson “Pete” Armstrong, a child prodigy with total recall memory, whose entire life’s outlook has been defined by the tragic murder of his younger brother, Leonard, by an ex-convict who was believed to be capable of committing violent crimes again, but could not be imprisoned any longer under the current law structure. Pete is committed to making a difference for humanity that will atone for his brother’s death and help millions of others, too. In his first year at Harvard at the age 13, Pete is recruited to enroll in a small, but exclusive, class of the brightest and most agile students on campus. In that class, he meets people and establishes friendships that will further his identity. It is there that the idea of a ‘truth machine’ is conceived and Pete realizes that its existence is possible and that he could do it. The ‘truth machine’ would be a mechanism that would be 100% accurate in determining if a person was lying or telling the truth. It could help eliminate crime and dishonesty in general. As long as it is employed universally (and not just by government officials), the ‘truth machine’ could revolutionize humanity and take it to that next evolutionary step which would help it avert its coming self-destruction.

The protagonist places a back door in the book’s otherwise infallible lie detector, allowing him to avoid detection when he repeats fragments of Walt Whitman’s poem “O Captain! My Captain!” in his mind.

果能斷乎？☺

Poolala (talk) 18:41, 22 September 2013 (UTC)

Weird! I am also working on a truth machine!

This version only accepts 1 and 0 as input, otherwise it starts again.

      <
 ====="
   >-[!+>:<
   "==#====
>;[!: Truth
===#=Machine

rock64@rock64:~/mlc ./a.out 
x
0 rock64@rock64:~/mlc ./a.out 
1
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ^C

最後我們介紹一下『何謂 Thue 之改寫系統』？結束這個《系列》的第一篇。阿克塞爾‧圖厄【挪威語 Axel Thue】一位數學家，以研究丟番圖用『有理數』逼近『實數』問題以及開拓『組合數學』之貢獻而聞名。他於一九一四發表了『詞之群論問題』Word problem for group 啟始了一個今天稱之為『字串改寫系統』SRS String Rewriting System 的先河，如從現今的研究和發現來看，它與圖靈機的『停機問題』密切相關。上個千禧年之時，John Colagioia 用『Semi-Thue System』寫了一個『奧秘的』 esoteric 程式語言 Thue ，作者宣稱︰

Thue represents one of the simplest possible ways to construe 『constraint-based』基於約束 programming. It is to the constraint-based 『paradigm』典範 what languages like『 OISC 』── 單指令集電腦 One instruction set computer ── are to the imperative paradigm; in other words, it’s a 『tar pit』焦油坑.

─── 《THUE 之改寫系統《一》》

如何思考用 racket 語言建置之 MarioLANG 是否『圖靈完備』呢？

Turing completeness

In computability theory, a system of data-manipulation rules (such as a computer’s instruction set, a programming language, or a cellular automaton) is said to be Turing complete or computationally universal if it can be used to simulate any Turing machine. This means that this system is able to recognize or decide other data-manipulation rule sets. Turing completeness is used as a way to express the power of such data-manipulation rule set. The expression power of these grammars is captured in the Chomsky hierarchy. Virtually all programming languages today are Turing Complete. The concept is named after English mathematician and computer scientist Alan Turing.

A closely related concept is that of Turing equivalence – two computers P and Q are called equivalent if P can simulate Q and Q can simulate P. The Church–Turing thesis conjectures that any function whose values can be computed by an algorithm can be computed by a Turing machine, and therefore that if any real-world computer can simulate a Turing machine, it is Turing equivalent to a Turing machine. A universal Turing machine can be used to simulate any Turing machine and by extension the computational aspects of any possible real-world computer.^{[NB 1]}

To show that something is Turing complete, it is enough to show that it can be used to simulate some Turing complete system. For example, an imperative language is Turing complete if it has conditional branching (e.g., “if” and “goto” statements, or a “branch if zero” instruction; see one instruction set computer) and the ability to change an arbitrary amount of memory (e.g., the ability to maintain an arbitrary number of data items). Of course, no physical system can have infinite memory; but if the limitation of finite memory is ignored, most programming languages are otherwise Turing complete.

面對『 esoteric 』焦油坑，最好留之於『奧秘』乎？？

Thue (/ˈtuːeɪ/ TOO-ay) is an esoteric programming language invented by John Colagioia in early 2000. It is a meta-language that can be used to define or recognize Type-0 languages from the Chomsky hierarchy. Because it is able to define languages of such complexity, it is also Turing-complete itself. Thue is based on a nondeterministic string rewriting system called semi-Thue grammar, which itself is named after the Norwegian mathematician Axel Thue.

※ 註︰

catseye/Thue

Cat’s Eye Technologies’ distribution of John Colagioia’s Thue programming language http://catseye.tc/node/Thue

The Thue Programming Language

This is Cat’s Eye Technologies’ distribution of Thue, an esoteric programming language designed by John Colagioia. Thue is a non-deterministic string-rewriting language, based on a formalism called a semi-Thue system, but also including some programming-oriented features, like input and output.

The specification can be found in the file thue.txt in the doc directory.

John’s implementation of the language, in C, is in the file thue.c in the src directory, and can, for all intents and purposes, be considered the reference implementation. There is no Makefile but an executable can be built by running the included build.sh script, which is trivial.

In the src directory, there are also two other implementation of Thue:

• thue.py, in Python, written by Frédéric van der Plancke
• thue.rb, in Ruby, written by Chris Pressey

There is an assortment of example Thue programs in the eg directory. The credits for these are as follows:

• add_bin.t: Frédéric van der Plancke
• edgcase?.t: Chris Pressey
• truth-machine.t: Keymaker
• quine.t: TSUYUSATO Kitsune
• all others: John Colagioia

More information on Thue can be found on the esolangs.org wiki entry for Thue.

Contents in this distribution are “essentially in the public domain” (scare quotes intentional.) See the file LICENSE for more information.

那邊『同一性』identity 問題，嘎天震響已久！

這個『同一性』identity 問題，在邏輯學上叫做『同一律』，與真假不相容的『矛盾律』齊名︰

。

這裡『邱奇－圖靈論題』尚未證明！！

同樣的問題也發生在計算機科學中的『同等』之『可計算性』問題之上，如果有甲和乙兩台計算機，或者說假使有  A 與 B 兩個程式語言，你將如何區分它們彼此的『計算的功能』或者『表達之能力』的呢？有一個尚未被證明的著名『猜測』，一個由『 λ 運算』之創始人 Church 和『圖靈機』的發明者 Turing 共通設想的『論題』 thesis ︰

 In computability theory,  the Church–Turing thesis ( also known as the Turing–Church thesis,  the Church–Turing conjecture,  Church’s thesis,  Church’s conjecture,  and Turing’s thesis) is a combined hypothesis ( “thesis” ) about the nature of functions whose values are effectively calculable;  or,  in more modern terms,  functions whose values are algorithmically computable.  In simple terms,  the Church–Turing thesis states that a function is algorithmically computable if and only if it is computable by a Turing machine.

因此任何計算機或程式語言只要能夠『模擬』simulate 『圖靈機』，按造上述猜測，它們都具有一樣的『計算能力』，所以 Thue 之改寫系統也具有同等的計算能力。如果你試著去讀 John Colagioia 所寫的 Thue 語言的  python  原始碼，不知會不會驚訝於包含著註解，程式全長只有二百九十二行，但它和 python 語言的計算能力竟是一樣的。但是不要『誤解』這個計算能力的『相當性』，並不代表著『程式寫作』的『方便性』或『清晰性』，就像 Log 『計算尺』的發明，是因為在用紙筆計算的時代，大數的乘除有時甚至是不可能的。舉個例說計算 ，假使真的一個一個的乘，然後再加不知要不要花上『千萬年』，但是如果使用 Log ，可能是『幾分鐘』的事。也許有人反對說，兩個結果不一樣，一個是『正確的』數，另一個只是『近似的』值，這也難怪有人不得不用 『奧秘的』語法寫一個『神奇的』程式︰『我愛你一世，唉！我氣你愛』，看看會不會發生不可判定之『當機』問題。

一九七二年布萊恩‧柯林漢 Brian Wilson Kernighan  於貝爾實驗室撰寫《Introduction to the Language B》的內部技術文件時，寫了一個『hello, world』的範例程式。其後他與 丹尼斯‧里奇 Dennis M. Ritchie 合著的《The C Programming Language》也保留了這個範例程式。不知怎的這成了一個『傳統』，成了初學者所編寫的第一個程式。現今流行的寫法是『Hello, World!』，不知柯林漢會不會抱怨這是是那個嗎？它的原典是︰

hello, world

，裡頭所有字母全是小寫，『 , 』之後有一『空白』。

Colagioia 的 Thue 語言是 semi-Thue 的字串改寫系統 ── 包含子字串擴充之 系統 ──，它的程式架構只有兩個部份 ── 字串改寫規則定義和初始字串構成 ──；其中『  字串改寫規則』的定義寫作︰

u ::= v

它提供了輸出入功能的『預設』符號 ，用『 ~ 』表示輸出和『 ::: 』表輸入，它們的規定是︰

標籤字串 ::= ~取代標籤之字串

， 意義是將『標籤字串』改寫成『空字串』，把接在『 ~ 』之後的『取代標籤之字串』輸出到『標準輸出』── 一般是顯示器 ──。

標籤字串 ::=:::

，意義是將『標籤字串』由『標準輸入』── 一般是鍵盤 ── 之輸入取代。

改寫規則定義的『結束列』是一條『空白的規則』定義列︰

::=

，它結束了改寫規則之定義，開啟了『初始字串』的構成。Thue  語言方便讓你可以寫多列的字串，它的語言解譯器會自動將它們序連串成一整個『初始字串』。

一個程式語言的寫作規則只有『四條』，它真的『能寫程式』嗎？當然能，而且可以用『中文化』的『符號』或者說『概念』來寫程式，舉個例子『將一個使用者輸入的二進制之數加一』可以寫成︰

1後繼者::=1加一
0後繼者::=1
01加一::=10
11加一::=1加一0
後繼者0::=後繼者
後繼者1加一::=10
□::=:::
::=
後繼者□後繼者

，這裡的『後繼者』第一個意思是一種自然數的概念，是義大利數學家 Giuseppe Peano 提出的概念︰

自然數 n 的後繼者是 n + 1

，假使它用在『0』與『1』的符號之後，表示將『之前』的數『加一』；如果它用在『0』與『1』的符號之前，是對『之後』之數作最後的『進位』處理。假使你試著用 Step 按鍵，一步一步的觀察，你將能發現這個 Thue 程式的『奧秘』。事實上有許多的『概念』可以用『各種』之『表述』形式，只看用這個概念的人到底是如何設想的呢？更不要說『人類的語言』之本身當然是能『寫作程式』的啊！！

有許多的人以為『確定性』要比『隨機性』要困難的多，其實是『隨機性』真實要困難的多。試想你要怎麽『產生』它的呢？再想一想所謂的『亂數產生器』Random number generation 的方法，它的背後有個『公式』，『隨機』真是能有公式的嗎？所以通常會將之冠以『 pseudo 』一詞，表達著不是像《易經》說的那樣『陰陽不測謂之神』。Thue 之改寫系統的『不確定性』是否就能『心誠則靈』的呢？不如就『擲個筊』吧！

擲筊::=~聖杯
擲筊::=~無杯
誠心祈求::=誠心擲筊祈求
::=
誠心擲筊祈求

── 原來『道可道，非常道』一樣是『程式之道』的啊！！ ──

─── 摘自《THUE 之改寫系統《三》》

或該擲筊耶◎

古人說︰熟讀唐詩三百首，不會作詩也會吟。就像能寫小說的少，會讀小說的多。鏡花緣演繹『熟能生巧』，自有其理也。

─── 《L4K ︰ 通往 PYTHON 的道路 ── RUR-PLE 斟酌》

祇為一時手癢，好奇 MarioLANG 如何『打招呼』呢？

Good sample programs

Is anyone willing to make any of the classic program examples in this language, like Hello World, Cat Programs, or working 99 Bottles programs? —JWinslow23 (talk) 18:23, 21 September 2013 (UTC)

I created a Hello World program (hoping MarioLANG won’t crash when faced with ＄s and letter characters).

               MarioLANG Hello World    <
         = =============================^<
           |   Created by JWinslow23   |=^<
         = ==============================="=
++++++++++
========== =
          >)+++++++)++++++++++)+++)+((((-[!)++.)+.
         =================================#======= =
  .------.+++.).+++++++++++++++((.++).+++..+++++++<
= ==================================================
 >--------.)+.).
================ =        |*
                         
      
      
 
      
 
               =========== ======

Anyone have any others? —JWinslow23 (talk) 19:31, 21 September 2013 (UTC)

I suspect the letters will work fine as the spec says unknown characters are comments. I am more uncertain about your castle made of elevators. 😛

However, the original author never fleshed out everything exactly, and hasn’t been seen in 3 years. His website is dead (and not on Wayback) and I don’t remember him making any interpreter, so in my opinion whoever actually makes one gets to decide the missing details. —Ørjan (talk) 23:42, 21 September 2013 (UTC)

Oerjan, I didn’t mean to make the castle out of elevators. I’ll change it to more semantics.rkt
#lang racket

(provide (all-defined-out))

(struct env (memory heading skip?) #:mutable #:transparent)
(struct mem (byte previous next) #:mutable)
(struct cell (char [left #:mutable] [up #:mutable] [right #:mutable] [down #:mutable])
#:prefab)

(define (new-env)
(env (mem 0 #f #f) ‘right #f))

(define (decrease-pointer env)
(let ([pos (env-memory env)])
(when (eq? (mem-previous pos) #f)
(set-mem-previous! pos (mem 0 #f pos)))
(set-env-memory! env (mem-previous pos))
env))

(define (increase-pointer env)
(let ([pos (env-memory env)])
(when (eq? (mem-next pos) #f)
(set-mem-next! pos (mem 0 pos #f)))
(set-env-memory! env (mem-next pos))
env))

(define (update-byte! env func)
(let ([memory (env-memory env)])
(set-mem-byte! memory (func (mem-byte memory)))))
…
(define (exec-instruction cell env)
(if (env-skip? env)
(set-env-skip?! env #f)
(case (cell-char cell)
[(#\+) (update-byte! env add1)]
[(#\-) (update-byte! env sub1)]
[(#) (increase-pointer env)]
[(#\.) (write-byte (mem-byte (env-memory env))) (flush-output)]
[(#\:) (write-string (format “~a” (mem-byte (env-memory env))) (current-output-por
t))]
[(#\,) (set-mem-byte! (env-memory env) (read-byte (current-input-port)))]
[(#\;) (set-mem-byte! (env-memory env) (read (current-input-port)))]
[(#\>) (set-env-heading! env ‘right)]
[(#\<) (set-env-heading! env ‘left)]
[(#\@) (set-env-heading! env (case (env-heading env)
[(right) ‘left] [(left) ‘right]
[else (env-heading env)]))]
[(#\!) (set-env-heading! env #f)]
[(#\[) (when (= (mem-byte (env-memory env)) 0)
(set-env-skip?! env #t))])))
…
 

莫非這樣仍巧得

Turing-complete

Relationship to computation

One of the more common misconceptions about Turing-completeness is that it is something that is required to perform any sort of computations (and that, conversely, any system that can perform some computations is Turing-complete.)

This is not the case when talking about a restricted set of computations. A finite-state automaton, for example, can be constructed which computes the Ackermann function f(m, n) for 1 < m < 1000 and 1 < n < 1000. In fact, such an evaluation could be stored in a million-cell lookup table.

This issue is further explored in the next section.

Relationship to the physical world

Turing-completeness applies to abstract systems (such as languages and formal automata) but not to real ones (such as computers and interpreters.) Physical machines have the following properties:

• they do not have unbounded storage space; and
• they eventually break down.

For these reasons, it should be obvious that no actual computer can be Turing-complete. However, it is also obvious that physical computers are perfectly capable of performing practical, finite computations in spite of that.

By extension, implementations of languages (compilers and interpreters) on physical computers are also not Turing-complete, but are nonetheless capable of specifying computations.

Therefore, it can be useful to make a distinction between being “usable for computation” and being Turing-complete. A language can be “usable for computation” while not being Turing-complete; all Turing-complete systems are “usable for computation”, however.

SMETANA is “usable for computation”, in that it is limited only by the code size of the program one chooses to write. Arguments have been made that Malbolge is also “usable for computation.”

A formal definition of “usable for computation” is currently being sought.

Overspecification

Often, a programming language is “after the fact” in that its specification comes from an attempt to describe the behavior of an implementation of that language.

As has just been noted, such implementations, being based as they are on physical machines, cannot be Turing-complete. So when this is done, there is a danger that the language will be overspecified, and that limitations of the physical machine will be reflected in the description of the language. This, often needlessly, causes the language to fail to be Turing-complete.

An interesting example of this is the C programming language. The C specification requires an integer result from sizeof() operator. The sizeof() operator’s result is an unsigned integer, of type size_t, for ANSI C, or an int or long for traditional C. The range of these integers is bounded. Since the sizeof() any object in a C implementation must be a finite size, then C cannot be Turing-complete, because it cannot address an unbounded storage space.

There are sometimes ways out of this. If a language specification requires that the size of some address (for example) be “implementation-dependent but no less than 16 bits” then one can argue that there exists an “implementation” where the size of addresses is unbounded, and that this “implementation” is Turing-complete. (That is, provided that the concept of an “implementation” which can never be implemented on a real computer is unproblematic.)

………

『歸結』耶？

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

拉丁語 tertium non datur 聲稱︰

任何命題 必真。

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

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

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

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

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

『單磁帶』one-tape 圖靈機是一個有序七元組 ，此處

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

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

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

是不包含空白符號的『輸入符號』集合

是『初始狀態』

是『最終狀態』或稱作『接受狀態』，一般可能有

是稱作『轉移函式』transition function，其中 代表『讀寫頭』之向『左，右』移動，還有的增加了『不移動』no shift 的擴張

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

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

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

mlang/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

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世紀上半葉，對可計算性進行公式化表示的嘗試有：

• 美國數學家阿隆佐·邱奇創建了稱為λ演算的方法來定義函數。
• 英國數學家阿蘭·圖靈創建了可對輸入進行運算的理論機器模型，現在被稱為通用圖靈機。
• 邱奇以及數學家史蒂芬·科爾·克萊尼和邏輯學家J. Barkley Rosser一起定義了一類函數， 這種函數的值可使用遞歸方法計算。

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

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

假說前提

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

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

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

正式闡述

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

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

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

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

這可以轉述如下：

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

圖靈則是如此描述的：

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

雖很重要，暫且放下☺

假使說給定了一個『 λ表達式』 ，有人『第一步』這樣作『 化約』︰

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

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

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

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

是指表達式 是經由表達式 中的某一函式應用子表達式 『 化約』而得來。假使『約定』零步 化約是說 『』，這樣我們就可以說『單步』或『多次單步』之『單步 化約』的『化約封閉性』︰

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

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

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

【Church-Rosser 定理】說

如果 而且 ；那麼就會存在一個 ， 使得 以及 。

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

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

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

二、如果 是一個『 正規元型』，

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

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

用『左』策略會得到『上圖』，用『右』策略會卡在 。

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

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

一、 ，無條件自反律

二、 ，對稱律

三、 ，遷移律

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

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

一、 ，『應用』於『等式』之『結果』相等

二、 ，『等式』之『函式』的『應用』相等

三、 ，『等式』之『函式抽象』相等

四、 ，『應用』是無條件的『化約相等』

五、 擴張， ，『外延』相同的『函式』相等

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

知道 是什麼。且能將之聯繫上 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

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:

Think substitution via tree surgery, preserving bindings

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

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

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.

未曾深研，不敢亂講呦。