私は最近、Haskell と Agda (従属型関数型プログラミング言語) を取り上げた大学のコースを修了しましたが、これらのラムダ計算を組み合わせロジックに置き換えることができるかどうか疑問に思っていました。Haskell では、これは S および K コンビネータを使用して可能であるように思われるため、ポイントフリーになります。アグダに相当するものは何だろうと思っていました。つまり、依存型の関数型プログラミング言語を、変数を使用せずに Agda と同等のものにすることはできますか?
また、どうにかして定量化をコンビネータに置き換えることは可能ですか? これが偶然かどうかはわかりませんが、たとえば全称量化により、型シグネチャがラムダ式のように見えます。意味を変えずに型シグネチャから全称量化を削除する方法はありますか? 例:
forall a : Int -> a < 0 -> a + a < a
forallを使わずに同じことを表現できますか？
それで、もう少し考えて、少し前進しました。これは、Martin-Löf の非常に単純な (しかし一貫性のない)Set : Setシステムを組み合わせスタイルでエンコードする最初の試みです。終了するのは良い方法ではありませんが、開始するのに最も簡単な場所です。この型理論の構文は、型注釈、Pi 型、およびユニバース Set を使用した単なるラムダ計算です。
完全を期すために、ルールを提示します。コンテキストの有効性は、s に存在する新しい変数を隣接させることによって、空からコンテキストを構築できることを示していますSet。
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ます。
(脱線. 抽象化の型を合成できるようにする場合は、ラムダの型注釈が必要です。手口として型チェックに切り替える場合でも、 のようなベータ版をチェックする注釈が必要です。(\ x -> t) s全体の型から部分の型を推測する. 私は現代の設計者に、型をチェックし、まさに構文からベータ版を除外することをお勧めします.)
(余談。このシステムはSet:Set、さまざまな「嘘つきのパラドックス」の符号化を可能にするため、一貫性がありません。Martin-Löf がこの理論を提案したとき、ジラールは彼自身の一貫性のないシステム 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には よりも 1 つ多くの要素があり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に持ち上げるために使用されます。AG
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 の使用に関する型注釈を付けることを要求し、派生を効果的に記録することです。しかし、それは別のワームの缶です...
開始するのに十分熱心である場合は、ここで停止するのに適しています。残りは「舞台裏」のものです。
関連する型理論用語からブラケット抽象化変換を使用して、これらの組み合わせ型を生成しました。私がどのようにそれを行ったかを示し、この投稿が完全に無意味ではないことを示すために、私の機器を提供させてください.
次のように、コンビネータの型をパラメータで完全に抽象化して記述できます。pilPi と 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)
これらを定義して、関連するオープンサブタームを抽出し、翻訳を実行しました。
ビルド方法は次のとおりpilです。まず、Fin変数に使用するアイテム セットのクラスを定義します。そのようなすべてのセットには、上記のセットへのコンストラクター保存embエッジと新しいtop要素があり、それらを区別できます。embd関数は、値が のイメージにあるかどうかを示しますemb。
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
もちろん、FinforZeと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
これで、弱化操作を使用して、以下を定義できます。
class (Fin x, Fin y) => Le x y where
wk :: x -> y
関数は の要素を の最大の要素としてwk埋め込む必要があります。これにより、 の余分なものが小さくなり、de Bruijn インデックスの用語では、より局所的にバインドされます。xyy
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
そして、それを整理したら、ランクnのスカルダガリーが残りを行います.
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)
高階関数は、変数を表す用語を提供するだけでなく、変数が表示される任意のスコープで変数の正しい表現になるオーバーロードされたものを提供します。つまり、さまざまなスコープを型で区別するのに苦労したという事実は、 de Bruijn 表現への変換に必要なシフトを計算するのに十分な情報を Haskell 型チェッカーに与えます。なぜ犬を飼って吠えるのですか？
「ブラケットの抽象化」は、状況によっては依存型に対しても機能すると思います。次の論文のセクション 5 で、いくつかの K 型と S 型を見つけます。
法外だが意味のある偶然の一致
依存型の安全な構文と評価
Conor McBride、University of Strathclyde、2010
ラムダ式を組み合わせ式に変換することは、自然演繹証明をヒルベルト式証明に変換することにほぼ対応します。