[解決済み] 直観主義型理論の組合せ論的等価性とは？

質問

最近、大学の授業で Haskell と Agda (依存型関数型プログラミング言語) を取り上げられたのですが、これらのラムダ計算を組合せ論理で置き換えることが可能かどうか疑問に思っています。Haskellの場合、SとKの組み合わせで無点化できるようです。Agdaの場合はどうなんだろう？つまり、変数を使わずにAgdaと同等の依存型関数型プログラミング言語を作ることはできるのでしょうか？

また、数量化を組み合わせで置き換えることは可能でしょうか？偶然かどうかわかりませんが、例えば普遍的な数量化は型シグネチャをラムダ式のように見せてしまいます。意味を変えずに型シグネチャから普遍的な数量化を取り除く方法はないでしょうか？例えば、で。

forall a : Int -> a < 0 -> a + a < a

forallを使わなくても同じことが表現できるのでしょうか？

どのように解決するのですか？

そこで私はもう少し考え、少し前進しました。Martin-Löf の楽しくてシンプルな (しかし一貫性のない) エンコードの最初の刺客は次のとおりです。 Set : Set システムを組み合わせスタイルでエンコードしてみました。これを完成させるのは良い方法とは言えないが、始めるには一番簡単な場所だ。この型理論の構文は、型注釈、パイ型、およびユニバースセットを持つラムダ計算だけです。

ターゲット型理論

念のため、ルールを提示しておきます。コンテキストの有効性は、空のコンテクストから Set s.

                     G |- valid   G |- S : Set
--------------     ----------------------------- x fresh for G
  . |- valid         G, x:S |- valid

そして今、私たちは、どのように任意のコンテクストにおける用語の型を合成するか、そしてどのようにそれが含む用語の計算的振る舞いまで何かの型を変更するかを言うことができます。

  G |- valid             G |- S : Set   G |- T : Pi S \ x:S -> Set
------------------     ---------------------------------------------
  G |- Set : Set         G |- Pi S T : Set

  G |- S : Set   G, x:S |- t : T x         G |- f : Pi S T   G |- s : S
------------------------------------     --------------------------------
  G |- \ x:S -> t : Pi S T                 G |- f s : T s

  G |- valid                  G |- s : S   G |- T : Set
-------------- x:S in G     ----------------------------- S ={beta} T
  G |- x : S                  G |- s : T

オリジナルからの小さなバリエーションで、私はlambdaを唯一の結合演算子にして、Piの第2引数は戻り値の型が入力に依存する方法を計算する関数であるべきだとしました。慣習として（例えばAgdaでは、しかし悲しいことにHaskellではそうではありません）、ラムダのスコープは可能な限り右方向に拡張されるので、高階演算子の最後の引数であるとき、しばしば抽象化をブラケットしないでおくことができます：私がPiでそれをしたのがわかるでしょう。あなたのAgda型 (x : S) -> T は次のようになります Pi S \ x:S -> T .

( 余談 . ラムダに対する型アノテーションは、以下のようにしたい場合に必要です。 を合成する を合成できるようにするために必要である。もし、型に切り替えると をチェックする のようなβ-redexをチェックするためのアノテーションが必要です。 (\ x -> t) s のようなβ-redexをチェックするための注釈が必要です。私は、現代の設計者に、型をチェックし、まさに構文からβ-redexを除外するよう助言しています)。

( 余談 . このシステムは、以下のように矛盾しています。 Set:Set によって、様々な「嘘つきパラドックス」を符号化することができます。Martin-Löfがこの理論を提案したとき、Girardは彼自身の無矛盾なシステムUでそれを符号化したものを送りました。その後のHurkensによるパラドックスは、私たちが知る限り最もきちんとした毒のある構造です)。

コンビネーターの構文と正規化

ともあれ、PiとSetという2つの余分な記号があるので、S、Kと2つの余分な記号で組合せ翻訳がなんとかなるかもしれませんね。私は宇宙をU、積をPとしました。

今、私たちは（自由変数を持つ）型付けされていない組合せ構文を定義することができます。

data SKUP = S | K | U | P deriving (Show, Eq)

data Unty a
  = C SKUP
  | Unty a :. Unty a
  | V a
  deriving (Functor, Eq)
infixl 4 :.

型によって表される自由変数を含む手段を入れたことに注意してください。 a で表される自由変数を含む手段をこの構文に含めたことに注意してください。私の反射的な行動とは別に、（その名にふさわしい構文はすべて、自由モナドに return 変数を埋め込んだり >>= 置換を実行する)、結合を持つ用語をその結合形式に変換するプロセスの中間段階を表現するのに便利でしょう。

これが正規化です。

norm :: Unty a -> Unty a
norm (f :. a)  = norm f $. a
norm c         = c

($.) :: Unty a -> Unty a -> Unty a        -- requires first arg in normal form
C S :. f :. a $. g  = f $. g $. (a :. g)  -- S f a g = f g (a g)   share environment
C K :. a $. g       = a                   -- K a g = a             drop environment
n $. g              = n :. norm g         -- guarantees output in normal form
infixl 4 $.

(読者への課題として、まさに正規形に対する型を定義し、これらの操作の型をシャープにすることである)

型理論の表現

これで、型理論の構文を定義することができます。

data Tm a
  = Var a
  | Lam (Tm a) (Tm (Su a))    -- Lam is the only place where binding happens
  | Tm a :$ Tm a
  | Pi (Tm a) (Tm a)          -- the second arg of Pi is a function computing a Set
  | Set
  deriving (Show, Functor)
infixl 4 :$

data Ze
magic :: Ze -> a
magic x = x `seq` error "Tragic!"

data Su a = Ze | Su a deriving (Show, Functor, Eq)

私はBellegardeとHookの方法（BirdとPatersonによって広められた方法）でde Bruijnインデックス表現を使用しています。型は Su a は a というように、バインダーの下にある自由変数の型として使用します。 Ze を新しく束縛された変数として、そして Su x は古い自由変数のシフトされた表現です。 x .

用語のコンビネータへの変換

そして、これで通常の翻訳を取得します。 ブラケットの抽象化 .

tm :: Tm a -> Unty a
tm (Var a)    = V a
tm (Lam _ b)  = bra (tm b)
tm (f :$ a)   = tm f :. tm a
tm (Pi a b)   = C P :. tm a :. tm b
tm Set        = C U

bra :: Unty (Su a) -> Unty a               -- binds a variable, building a function
bra (V Ze)      = C S :. C K :. C K        -- the variable itself yields the identity
bra (V (Su x))  = C K :. V x               -- free variables become constants
bra (C c)       = C K :. C c               -- combinators become constant
bra (f :. a)    = C S :. bra f :. bra a    -- S is exactly lifted application

コンバイネータの入力

翻訳ではコンビネーターの使い方を示しており、その型がどうあるべきかの手がかりを与えてくれています。 U と P は単なるセット・コンストラクタなので、翻訳されていない型を書き、Piに "Agda記法"を許可すると、次のようになります。

U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set

は K コンビネータは，ある型の値を持ち上げるために使われます。 A を他の型に対する定数関数に変換します。 G .

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

は S コンビネータは、すべてのパーツが依存する可能性がある型上のアプリケーションを持ち上げるために使用されます。

  G : Set
  A : (g : G) -> Set
  B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
  S : (f : (g : G) ->    (a : A g) -> B g a   ) ->
      (a : (g : G) ->    A g                  ) ->
           (g : G) ->    B g (a g)

の型を見てみると S の型を見てみると、それがまさに 文脈に応じた という型理論の適用規則を正確に述べていることがわかります。したがって、これが適用構成を反映するのに適しているのです。これがその仕事です!

そうすると、閉じたものに対してのみ適用がある

  f : Pi A B
  a : A
--------------
  f a : B a

しかし、問題があります。私は組合せの型を組合せ型理論ではなく、普通の型理論で書いてしまったのだ。幸いなことに、翻訳してくれる機械がある。

組合せ型システム

---------
  U : U

---------------------------------------------------------
  P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU)))

  G : U
  A : U
-----------------------------------------
  K : P[A](S(S(KP)(K[G]))(S(KK)(K[A])))

  G : U
  A : P[G](KU)
  B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU)))
--------------------------------------------------------------------------------------
  S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK))))
      (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A])))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G]))))
      (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))
      (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))
      (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))

  M : A   B : U
----------------- A ={norm} B
  M : B

というわけで、読めない栄光がここにあります。 Set:Set !

まだ少し問題があります。構文から推測して G , A と B のパラメータは S と同じように K についても同様で、単に用語から これに対応して、以下のことが確認できる。 型付け導出 をアルゴリズム的に検証することはできるが，元のシステムのようにコンビネータ項を型付けチェックすることはできない．うまくいくかもしれないのは，タイプチェッカーへの入力にSとKの使用に関する型注釈をつけることを要求し，効果的に導出を記録することである．しかし、それは別の問題である。

これは、あなたが始めるのに十分熱心であった場合、停止するのに良い場所です。残りは舞台裏の話です。

コンバイネータの型を生成する

私は、関連する型理論の用語からブラケット抽象化変換を使用して、これらの組み合わせの型を生成しました。私がどのように行ったかを示し、この投稿が全く無意味でないようにするために、私の装置を提供させてください。

私は、そのパラメータを完全に抽象化したコンビネーターの型を、次のように書くことができます。私は便利な pil 関数を使っている。これは Pi と lambda を組み合わせてドメイン型の繰り返しを避け、むしろ Haskell の関数空間を使って変数を束縛できるようにするものだ。おそらく、次のようにほとんど読み取れるでしょう!

pTy :: Tm a
pTy = fmap magic $
  pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set

kTy :: Tm a
kTy = fmap magic $
  pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A

sTy :: Tm a
sTy = fmap magic $
  pil Set $ \ _G ->
  pil (pil _G $ \ g -> Set) $ \ _A ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f ->
  pil (pil _G $ \ g -> _A :$ g) $ \ a ->
  pil _G $ \ g -> _B :$ g :$ (a :$ g)

これらを定義した上で、関連する オープン サブタームを抽出し、翻訳にかけました。

de Bruijn エンコーディングツールキット

ここでは pil . まず Fin iteの集合のクラスを定義します。このような集合には、コンストラクタを保持する emb を上記の集合に追加し、さらに新しい top 要素が追加され、それらを見分けることができます。 embd の画像に値があるかどうかを教えてくれる関数です。 emb .

class Fin x where
  top :: Su x
  emb :: x -> Su x
  embd :: Su x -> Maybe x

もちろん Fin に対して Ze と Suc

instance Fin Ze where
  top = Ze              -- Ze is the only, so the highest
  emb = magic
  embd _ = Nothing      -- there was nothing to embed

instance Fin x => Fin (Su x) where
  top = Su top          -- the highest is one higher
  emb Ze     = Ze            -- emb preserves Ze
  emb (Su x) = Su (emb x)    -- and Su
  embd Ze      = Just Ze           -- Ze is definitely embedded
  embd (Su x)  = fmap Su (embd x)  -- otherwise, wait and see

これで、less-or-equals を定義できるようになりました。 <項目 弱体化 の操作になります。

class (Fin x, Fin y) => Le x y where
  wk :: x -> y

は wk の要素を埋め込む必要があります。 x を 最大の の要素である y の中にある余分なものがなくなるように y の余分なものは小さくなり、したがって de Bruijn 指数の用語では、より局所的に束縛されます。

instance Fin y => Le Ze y where
  wk = magic    -- nothing to embed

instance Le x y => Le (Su x) (Su y) where
  wk x = case embd x of
    Nothing  -> top          -- top maps to top
    Just y   -> emb (wk y)   -- embedded gets weakened and embedded

そして、それを解決したら、あとはちょっとしたランク・アンド・スカルグレーショがやってくれるのです。

lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = Lam s (f (Var (wk (Ze :: Su x))))
pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
pil s f = Pi s (lam s f)

高階の関数は変数を表す項を与えるだけでなく オーバーロードされた を与えるだけでなく、その変数が見えるすべてのスコープでその変数を正しく表現するようになります。つまり、わざわざ異なるスコープを区別しているのは 型によって とすることで、Haskell の型チェッカは de Bruijn 表現への翻訳に必要なシフトを計算するのに十分な情報を得ることができるのである。なぜ犬を飼い、自分で吠えるのか？