如何系统地计算给定类型的居民人数？

如何系统地计算系统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

如何系统地计算给定类型的居民人数？

回答

相关问题