The Rise of Intuitionistic Logic
直構邏輯的崛起
Chinese version: here
英文版：這裡
In the first edition of Martin-Löf’s type theory preprinted in 1971, Martin-Löf introduced a universe, normally called \(\mathcal{U}\), in his theory.
It contains (i.e. is the type of) all types including the universe itself.
After the theory was quickly found to be inconsistent by Girard, Martin-Löf then presented a so called “predicative” theory, with a hierarchy of universes, each usually written with a subscript, e.g. \(\mathcal{U}_0\), \(\mathcal{U}_1\), \(\mathcal{U}_2\) …, and the type of each universe is the higher one universe.
So, for example, the type of \(\mathcal{U}_0\) is \(\mathcal{U}_1\), and the type of \(\mathcal{U}_1\) is \(\mathcal{U}_2\), and going on and on.
In this article, I exploit the need for (at least) one other hierarchy of universes, written \(..\mathcal{U}_n\), in which \(n\) is a natural number in the metatheory, as in the above notation \(\mathcal{U}_n\).
之前在講解Curry-Howard correspondence時
我用的理論基礎是CoC
而CoC最大的問題在於：
它無法證明數學歸納法
為什麼呢？
首先來看看CoC中的自然數
還記得我最最前面在untyped lambda那篇介紹的定義嗎……
這篇文章會討論有點不同的主題
從這個問題開始：
你要怎麼寫一個term
使得他的type為\(\forall X. X\)？
The first programming language that I learned seriously is Java.
I’ve quickly come out with an interpretation that whatever language features in Java correspond to parts of speech.
Variables are nouns;
this is the subject and the arguments after the name of the method call are objects;
methods are verbs and interfaces are adjectives.
在抽象代數中
一個很重要的概念是群(group)
一個群定義了一個集合和其上的一個二元運算的關係
在介紹群之前
我要先介紹比群更簡單的結構
1.1 The very idea of a category
1.2 The category of sets
1.3 More examples
新連載:D
先介紹一下這系列文章會出現的背景吧
PTS是lambda cube的再度延伸
在CoC中
\(\star\)和\(\Box\)被稱為sort
sort是什麼呢？
它是較低層一般型別的型別
舉例來說
\(\forall A. A \to A: \star\)
\(\star \to \star: \Box\)
但假如我們有個從一般kind到一般kind的lambda
它的型別不會是\(\Box\)
而會是\(\Box \to \Box\)
我決定重新來過
砍了整個repo
然後建立一個預設的新專案觀察一個Jekyll網站的架構
我想把部落格轉移到Jekyll
為什麼用Logdown撰寫文章不好呢？
原因有二：
看了一下
Jekyll實在很複雜
看起來是滿通用的一套架構
但也因為如此不好理解
我想先套用Jekyll Bootstrap
之後再慢慢修改它的程式碼使其符合自己需要
首先刪除掉原有repo的所有檔案
在命令提示字元中輸入
git clone https://github.com/plusjade/jekyll-bootstrap.git AndyShiue.github.io
cd AndyShiue.github.io
git remote set-url origin git@github.com:AndyShiue/AndyShiue.github.io.git
git push --force origin master
注意我事實上修改了一些部分
原本命令中的所有com都被我改成了io
另外push後面加了參數--force
這樣才對
現在我們要再加入term到type的函數
這樣的系統被稱為CoC(Calculus of Constructions)
來整理一下目前的狀況
開門見山
system F導入了type到term的函數
system Fω則再導入了type到type的函數
現在我們要導入type的型別
還記不記得一開始在用untyped lambda的時候是沒有型別的
這麼一來能寫出\(\Omega\)之類的無窮迴圈
假如type到type的函數是無型別的話
那不就也能在type階層上跑無窮迴圈了嗎QAQ
不……
在之前STLC的教學中
我們的世界被分成了兩個階層：term和type
接下來
我們會希望這兩者的差別變得更模糊
為什麼要這麼做？
因為lambda calculus可以被當作是程式語言的核心
在寫程式的時候
建立抽象是必要的過程
有了高層次的抽象
能讓不同的東西被視為一樣的
減少重複的冗餘程式碼
因此程式語言上也應該提供更高的抽象能力以幫助使用者
講完untyped lambda
接下來就要講typed lambda啦
顧名思義
typed lambda就是有type的lambda
因此必須要被type check
一個合理的type checker不會讓所有程式都type check成功
而是只接受特定的一些「正確的」程式
因此讓程式的錯誤能在編譯時期就被找出來
來寫教學吧
畢竟我最喜歡寫教學了…XD
這次要來說的是untyped lambda