λ→ à la Church 學習筆記-7（數據類型的表示）

目錄：類型論驛站寫作計劃

前一篇：λ→ à la Church 學習筆記-6（邏輯的表示）

這是我學習 λ→ à la Church 的最後一篇筆記。

在 中表示數據類型

定義1

1. 數據類型（data structure）是一個沒有特定關係（relations）的多類別（many-sorted）結構。數據結構里的類別被稱為數據集合（data set）。
2. 數據系統（data system）是數據結構的識別簽（signature）。數據系統里的類別被稱為數據類型（data type）。

例如：

• 類別：
• 函數：
• 常數：

上述數據系統可以用下圖來表示：

再比如，自然數的數據系統 可以表示為：

• 類別：
• 函數：
• 常數：

類別 上的列表 的數據系統可以表示為：

• 類別：
• 函數：
• 常數：

定義2（參數）

1. 如果數據系統里的某個類別沒有進來的箭頭，而且該類別沒有常量，則該類別被稱為參數類別（parameter sort）。
2. 如果一個數據系統沒有參數類別，我們稱這樣的數據系統為無參數（parameter-free）數據系統。

自然數系統是無參數數據系統；列表系統是以 為參數類別的有參數數據系統。

定義3（語言）

設 為一個數據系統，與其對應的語言 定義如下：

1. 的（開放）項模型（open termmodel），記為 ，包含 中的項（包含自由變數），以及函數符號給出的顯著映射（obvious map）。也就是說，對於 中的每一個類別 ，對應的集合 包含 中類別為 的所有項。和函數符號 相對應的函數 定義為 . 類別為 的常量 詮釋為自身： 。
2. 閉合項模型（closed termmodel），記為 ，參照上述定義定義。

例如自然數的閉合項模型包含集合 這個類型結構是 的同構副本（isomorphic copy）。

定義4（語境）

對於一個數據系統 ：

• ：參數類別
• ：其他類別
• 
• 
• 
• 

我們有語境（context）：

對於每一個項 ，我們定義 項 和語境 如下：

引理5

對於一個類型為 的項 ，我們有：

上面的翻譯方式比較直接，但是卻無法找到如 一樣的項，使得

原因是， 不過是一個變數，我們不能把複合項 或 分成各自的部分來探究他們所代表的數字之間的關係。所以我們需要一個更好的表示方法。

定義6

設 是按照定義4定義的數據系統。

1. （標記法）
2. d 表示包括：

• 類型 ，使得
• 項 ，使得
• 對於 的特定 表示，對於每一個項 ，我們定義 項 和語境 如下：

• 如果對於在 中的所有項 ，我們有 ， 那麼我們稱 的這個 表示是自由（free）的。

標記法7

設 是一個語境，我們有

定理8（Leivant 1983, B?hm-Berarducci 1985, Fokkinga 1987）

每一個數據系統 都有一個 的自由表示（free representation）。

實例：

列表（Lists）：

列表 以及 可以定義如下：

此外，

布爾值（Booleans）：

• 類別：
• 常量：

表示如下：

對子/二元組（Pairs）：

• 類別：
• 函數：

表示如下：

目錄：類型論驛站寫作計劃

前一篇：λ→ à la Church 學習筆記-6（邏輯的表示）