作者ephesians (ephesians)
看板PLT
標題[閒聊] 邏輯式語言與函數式語言
時間Sun Feb 25 04:24:03 2007
最近在涉獵另一種程式語言流派,
不是天流地流與神流,不是二刀流,也不是人稱一流劍一流,
是一種叫做函數式語言 (functional programming language) 的.
先聲明,因為以往工作與學習環境並不熟悉這東西的實作,
以下凡談到底層,含編譯/直譯等,都是胡扯瞎掰的.
如果有幸,將來可能有機會實作.
函數式語言的特色就是函數定義,寫完函數,程式就寫完了.
跟傳統程式語言 (結構化程式) 有什麼差別呢?
按數學來講,函數是指將定義域映射到值域,
而傳統程式語言的函數,除了映射之外,
還多了很多東西, (流程控制,例外處理,資源管理...等)
所以更稱為函式.
函數式語言沒有指定敘述,沒有副作用 (side effect), 也沒有流程控制.
可想而知,遞迴是函數式語言常用的東西,因為遞迴有隱性的流程控制功能.
這時候可能看棺...呃,看倌們會想到函數式語言程式有多慢,
但因為函數式語言沒有副作用,意指一個子函數只做它該做的事,其他不多做.
譬如隔壁 p 版正在討論的 int x=12; x=x+++++x; 疑義,
在函數式語言的世界是完全無效的!
哪個子運算式/子函數先計算,結果都一樣.
因此,一份函數呼叫可以被自由代換為它的函數內容,不改其義.
遞迴函數很慢,展開成非遞迴函數就快多了.
(甚至或許底層不需要有傳統語言編譯器的函式控制記憶區)
函數式語言之所以沒副作用,那是因為所有的變數一使用就不改其值.
沒有指定敘述可以修改變數內容.
接下來再講講邏輯式語言, (logical programming language)
邏輯語言的基本構件是邏輯式.
用過 Prolog 的人也許會覺得 a :- b, c. 是規則, (if b and c then a)
但這樣很容易陷入規則式推論系統的框架中,誤以為一旦使用 Prolog,
就非得實作規則式推論系統.
事實上,那是 !b || !c || a 這般邏輯式 (此式借用C的符號), 稱為Horn clause.
(Horn clause到底怎麼翻譯啊? 角句嗎?)
邏輯式語言的程式,就是許多邏輯式的集合,
稱為演繹式資料庫 (deductive database, DDB).
邏輯式語言的計算,在於掌握解集. (answer sets, 答案集)
回想范式圖 (Van diagram), 如果你有一則邏輯式 a :- (意指 a 恆真;已知 a),
你就會將一張代表宇集 U 的白紙劃為兩半,一半在線圈內,屬於 a/true 的範圍,
另一半在線圈外,屬於 ﹁a/false 的範圍.
當你有另一則邏輯式 b :-, 就在紙上畫另一個線圈.
加上一則邏輯式 c :- a, b, 是讓 a 線圈與 b 線圈有個交疊部份.
計算一則問題 ?- c 是與解集周旋,通過邏輯式的交叉火網,在那張白紙上畫地圖.
有些問題經計算後,會得到多種解集,譬如:
在DDB a :- ﹁b, c. b :- ﹁a, c. 中,
詢問 c 會得到 {a, ﹁b} 或 {﹁a, b} 二種解集.
解集的計算,稱為解集規劃 (answer set programming).
演繹式資料庫已經有一串發展脈絡,隨著邏輯式可用符號的增加,解集規劃也更複雜.
按著發展脈絡及系統層次,簡單地介紹於下:
1. DDB: 這個層次很低,很單純,沒有否定的述詞 (predictive).
2. Monotonic DDB: 改良 DDB 的缺點,增加了 ﹁ 符號,
其語意是指某述詞的存在不成立.
* DDB 與 MDDB 的層次相同,之後則是一層高於一層.
3. Extended Logic Programming (eLP, XD):
﹁ 符號的語意不夠完整. (試想想 "我不喜歡你" 與 "我沒有喜歡你" 的差別.)
因此,新的 not 符號誕生了,任務是明確表達某述詞的存在不存在都未定義.
述詞的否定符號優先順序是先判斷 not 述詞是 unknown,
再判斷 ﹁ 述詞是真的沒有.
4. Disjunctive Logic Programming: 終於可以使用 or 符號了.
5. Epistemic Logic Programming: 再加上一些很高階的符號,
例如 K 代表已知為真 (it's Known to be true),
M 代表必須為真 (it Must be true)
至於實作層面,不管是直譯或編譯皆可,想必都要附加一份引擎.
(流程控制不是該煩惱的事,函義/語意才是.)
相較之下,傳統程式語言不需要附加引擎,不過,所寫的程式本身就是引擎.
你要先把引擎的流程控制/副作用搞定. 辛苦的程式工人啊!
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 59.112.224.119
1F:推 semop:Horn clause 是以 Alfred Horn 為名的... 02/25 14:10
2F:→ ephesians:所以應該稱為Horn的句子 02/25 14:44