16

帰納的データ型とパターンマッチングの状態に関するAgdaマニュアル：

正規化を確実にするために、帰納的発生は厳密に正の位置に現れる必要があります。たとえば、次のデータ型は許可されていません。 

data Bad : Set where
  bad : (Bad → Bad) → Bad

コンストラクターへの引数にBadの負のオカレンスがあるためです。

誘導データ型にこの要件が必要なのはなぜですか？

4

2 に答える 2

14

指定したデータ型は、型指定されていないラムダ計算の埋め込みであるという点で特別です。

data Bad : Set where
  bad : (Bad → Bad) → Bad

unbad : Bad → (Bad → Bad)
unbad (bad f) = f

方法を見てみましょう。タイプされていないラムダ計算には次の用語があることを思い出してください。

 e := x | \x. e | e e'

[[e]]型なしラムダ計算項から型のAgda項への変換を定義できますBad（ただし、Agdaにはありません）。

[[x]]     = x
[[\x. e]] = bad (\x -> [[e]])
[[e e']]  = unbad [[e]] [[e']]

これで、お気に入りの非終了の型なしラムダ項を使用して、型の非終了項を生成できますBad。たとえば、次(\x. x x) (\x. x x)のタイプの非終了式に変換できBadます。

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x))

この型はたまたまこの引数にとって特に便利な形式でしたが、少しの作業で、再帰が負に発生する任意のデータ型に一般化できます。

于 2012-09-29T08:54:39.960 に答える
13

このようなデータ型によってどのような型にも生息できるようになる例は、Turner、DA（2004-07-28）、Total Functional Programming、sect。3.1、ルール2の758ページ：型の再帰は共変でなければなりません。」

Haskellを使ってもっと手の込んだ例を作ってみましょう。「悪い」再帰データ型から始めましょう

data Bad a = C (Bad a -> a)

そして、他の形式の再帰なしで、それからYコンビネータを構築します。これは、そのようなデータ型を持つことで、あらゆる種類の再帰を構築したり、無限の再帰によってあらゆる種類に生息したりできることを意味します。

型なしラムダ計算のYコンビネータは次のように定義されます。

Y = λf.(λx.f (x x)) (λx.f (x x))

その鍵は、でx自分自身に適用することですx x。型付き言語では、有効な型がない可能性があるため、これを直接行うことはできませxん。しかし、私たちのBadデータ型では、このモジュロでコンストラクターを追加/削除できます。

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

をとるx :: Bad aと、そのコンストラクターをアンラップして、内部の関数をxそれ自体に適用できます。これを行う方法がわかれば、Yコンビネータを簡単に構築できます。

yc :: (a -> a) -> a
yc f =  let fxx = C (\x -> f (selfApp x))  -- this is the λx.f (x x) part of Y
        in selfApp fxx

再帰的でも再帰的でもないselfAppycことに注意してください。関数自体への再帰的な呼び出しはありません。再帰は、再帰データ型でのみ表示されます。

構築されたコンビネータが実際に機能することを確認できます。無限ループを作ることができます：

loop :: a
loop = yc id

または計算して、 GCDとしましょう：

gcd' :: Int -> Int -> Int
gcd' = yc gcd0
  where
    gcd0  :: (Int -> Int -> Int) -> (Int -> Int -> Int)
    gcd0 rec a b  | c == 0     = b
                  | otherwise  = rec b c
      where c = a `mod` b
于 2012-09-29T08:21:05.927 に答える