如何系統地計算給定類型的居民人數？

如何系統地計算系統F中給定類型的居民人數？如何系統地計算給定類型的居民人數？

假設以下限制：

所有居民終止，即，沒有底部。
所有居民都沒有副作用。

例如（使用Haskell語法）：

Bool具有兩個居民。
(Bool, Bool)有四個居民。
Bool -> (Bool, Bool)有十六個居民。
forall a. a -> a有一個居民。
forall a. (a, a) -> (a, a)有四個居民。
forall a b. a -> b -> a有一個居民。
forall a. a沒有居民。

實現前三個算法是微不足道的，但我不知道如何去做其他的。

來源

2015-10-18 rightfold

我想解決同樣的問題。下面的討論無疑幫了我很多：

Abusing the algebra of algebraic data types - why does this work?

起初，我也被困擾的類型，如forall a. a -> a。然後，我有了一個頓悟。我意識到forall a. a -> a的類型是unit type的Mogensen-Scott encoding。因此，它只有一個居民。同樣，forall a. a是bottom type的Mogensen-Scott編碼。因此，它沒有居民。考慮下面的代數數據類型：

data Bottom       -- forall a. a 

data Unit = Unit     -- forall a. a -> a 

data Bool = False | True   -- forall a. a -> a -> a 

data Nat = Succ Nat | Zero   -- forall a. (a -> a) -> a -> a 

data List a = Cons a (List a) | Nil -- forall a b. (a -> b -> b) -> b -> b

的代數數據類型是一個products sum。我將使用語法⟦τ⟧來表示類型τ的居民人數。有兩種類型的我將在本文中使用：

系統F的數據類型，由下列BNF給出：
```
τ = α 
    | τ -> τ 
    | ∀ α. τ 
```

代數數據類型，由下列BNF給出：

τ = 
    | α 
    | τ + τ 
    | τ * τ 
    | μ α. τ

計算代數數據類型的居民的數目是非常直接的：

⟦⟧  = 
⟦τ¹ + τ²⟧ = ⟦τ¹⟧ + ⟦τ²⟧ 
⟦τ¹ * τ²⟧ = ⟦τ¹⟧ * ⟦τ²⟧ 
⟦μ α. τ⟧ = ⟦τ [μ α. τ/α]⟧

例如，考慮在列表數據類型μ β. α * β + 1：

⟦μ β. α * β + 1⟧ = ⟦(α * β + 1) [μ β. α * β + 1/β]⟧ 
       = ⟦α * (μ β. α * β + 1) + 1⟧ 
       = ⟦α * (μ β. α * β + 1)⟧ + ⟦1⟧ 
       = ⟦α⟧ * ⟦μ β. α * β + 1⟧ + ⟦1⟧ 
       = ⟦α⟧ * ⟦μ β. α * β + 1⟧ + 1

然而，計算系統F的數據類型的居民的數量不是那麼簡單的。儘管如此，它可以完成。爲此，我們需要將System F數據類型轉換爲等效的代數數據類型。例如，系統F數據類型∀ α. ∀ β. (α -> β -> β) -> β -> β等效於代數列表數據類型μ β. α * β + 1。

要注意的第一點是，雖然系統F型∀ α. ∀ β. (α -> β -> β) -> β -> β具有兩個萬向量詞還代數列表數據類型μ β. α * β + 1只有一個（固定點）量詞（即代數列表數據類型是單態）。

雖然我們可以使代數列表數據類型爲多態（即∀ α. μ β. α * β + 1）並添加規則⟦∀ α. τ⟧ = ∀ α. ⟦τ⟧，但我們不這樣做，因爲它不必要地使事情複雜化。我們假設多態類型專用於某種單形類型。

因此，第一步是刪除除了表示「定點」量詞之外的所有通用量詞。例如，類型∀ α. ∀ β. α -> β -> α變爲∀ α. α -> β -> α。

由於Mogensen-Scott編碼，大部分轉換都很簡單。例如：

∀ α. α      = μ α. 0     -- bottom type 

∀ α. α -> α     = μ α. 1 + 0    -- unit type 

∀ α. α -> α -> α    = μ α. 1 + 1 + 0   -- boolean type 

∀ α. (α -> α) -> α -> α  = μ α. (α * 1) + 1 + 0  -- natural number type 

∀ β. (α -> β -> β) -> β -> β = μ β. (α * β * 1) + 1 + 0 -- list type

但是，有些轉換並不那麼直接。例如，∀ α. α -> β -> α不代表有效的Mogensen-Scott編碼數據類型。

⟦∀ α. α -> β -> α⟧ = ⟦β -> ∀ α. α -> α⟧ 
        = ⟦∀ α. α -> α⟧^⟦β⟧ 
        = ⟦μ α. 1 + 0⟧^⟦β⟧ 
        = ⟦μ α. 1⟧^⟦β⟧ 
        = ⟦1⟧^⟦β⟧ 
        = 1^⟦β⟧ 
        = 1

對於其他類型的，我們需要使用一些詭計：不過，我們可以通過雜耍類型位得到正確的答案

∀ α. (α, α) -> (α, α) = (∀ α. (α, α) -> α, ∀ α. (α, α) -> α) 
         = (∀ α. α -> α -> α, ∀ α. α -> α -> α) 

⟦∀ α. α -> α -> α⟧ = ⟦μ α. 1 + 1 + 0⟧ 
        = ⟦μ α. 2⟧ 
        = ⟦2⟧ 
        = 2 

⟦∀ α. (α, α) -> (α, α)⟧ = ⟦∀ α. α -> α -> α⟧ * ⟦∀ α. α -> α -> α⟧ 
         = 2 * 2 
         = 4

雖然有一個簡單的算法，這將給我們數的Mogensen-Scott編碼類型的居民，但我想不出任何通用算法，它會給我們任何多態類型的居民數量。事實上，我有一個非常強烈的直覺，即計算任何多態類型的居民總數是一個不可判定的問題。因此，我相信沒有算法可以給我們一般多態類型的居民的數量。

儘管如此，我相信使用Mogensen-Scott編碼類型是一個很好的開始。希望這可以幫助。

來源

2015-10-19 07:04:26

如何系統地計算給定類型的居民人數？

回答

相關問題