直觉型理论的组合逻辑等价物是什么?

我最近完成了一门以Haskell和Agda(一种依赖types的函数式编程语言)为特色的大学课程,并且想知道是否可以用组合逻辑来替代这些中的lambda演算。 对于Haskell来说,使用S和K组合器似乎是可能的,从而使其不存在任何问题。 我想知道Agda的等价物是什么。 也就是说,能不能使用任何variables就可以生成一个与Agda相当的函数式编程语言?

另外,是否有可能以某种方式取代组合器的量化? 我不知道这是否是巧合,但是例如通用量化使得types签名看起来像一个lambdaexpression式。 有没有办法从types签名中去除通用量化而不改变其含义? 例如:

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

同样的事情可以不使用forall来expression吗?

所以我想了一下,取得了一些进展。 这是Martin-Löf以一种组合风格编码的令人愉快的简单(但不一致)的Set : Set系统的第一次尝试。 这不是一个好的方法来完成,但这是最容易入门的地方。 这种types理论的语法只是带有types注释的lambda-calculus,Pitypes和一个Universe Set。

目标types理论

为了完整起见,我会提出规则。 上下文有效性只是说你可以通过邻接Set的新variables来创build空的上下文。

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

现在我们可以说如何在任何给定的上下文中综合术语的types,以及如何改变某些东西的types直到它所包含的术语的计算行为。

  G |- valid G |- S : Set G |- T : Pi S \ x:S -> Set ------------------ --------------------------------------------- G |- Set : Set G |- Pi ST : Set G |- S : Set G, x:S |- t : T x G |- f : Pi STG |- s : S ------------------------------------ -------------------------------- G |- \ x:S -> t : Pi STG |- fs : T s G |- valid G |- s : SG |- T : Set -------------- x:S in G ----------------------------- S ={beta} T G |- x : SG |- s : T 

从原来的一个小的变化,我做了lambda唯一的绑定运算符,所以Pi的第二个参数应该是一个函数计算返回types依赖于input的方式。 按照惯例(例如,在Agda中,可惜不在Haskell中),lambda的范围尽可能地向右延伸,所以当它们是高阶运算符的最后一个参数时,通常可以将其抽象为无括号:您可以看到我做了与丕。 你的Agdatypes(x : S) -> T变成Pi S \ x:S -> T

Digression 。如果你希望能够综合抽象types,那么在lambda上input注释是必须的,如果你改用types检查作为你的工作方式,你仍然需要注释来检查一个beta-redex,例如(\ x -> t) s ,因为你无法从整体上猜测零件的types,所以我build议现代devise者检查types,并从句法中排除beta-redex。

Digression 。这个系统是不一致的,因为Set:Set允许编码各种各样的“说谎者悖论”。当Martin-Löf提出这个理论时,Girard给他发了一个在他自己的不一致的System U中的编码。 Hurkens是我们知道的最有毒的build筑。)

组合器语法和规范化

无论如何,我们有两个额外的符号,Pi和Set,所以我们也许可以用S,K和两个额外的符号来pipe理一个组合的翻译:我selectU代表宇宙,P代表产品。

现在我们可以定义无types的组合语法(带有自由variables):

 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在这种语法中包含由typesa表示的自由variables的方法。 除了作为我的一个reflection(每一个值得名称的语法都是一个带有returnembeddedvariables的自由monad和>>= perfoming的替代),在转换与其绑定的术语的过程中代表中间阶段是很方便的组合forms。

这是标准化:

 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 CS :. f :. a $. g = f $. g $. (a :. g) -- S fag = fg (ag) share environment CK :. a $. g = a -- K ag = a drop environment n $. g = n :. norm g -- guarantees output in normal form infixl 4 $. 

(读者的练习是为正常forms定义一个types,并强化这些操作的types。)

代表types理论

现在我们可以为我们的types理论定义一个语法。

 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) 

我使用贝尔加德和胡克的方式(如鸟和帕特森普及)的德Bruijn指数表示。 Suatypes比Su a有更多的元素,我们用它作为绑定下的自由variablestypes, Ze是新绑定的variables, Su x是旧自由variablesx的移位表示。

将术语翻译成组合器

而这样做,我们获取通常的翻译,基于括号抽象

 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 ab) = CP :. tm a :. tm b tm Set = CU bra :: Unty (Su a) -> Unty a -- binds a variable, building a function bra (V Ze) = CS :. CK :. CK -- the variable itself yields the identity bra (V (Su x)) = CK :. V x -- free variables become constants bra (C c) = CK :. C c -- combinators become constant bra (f :. a) = CS :. bra f :. bra a -- S is exactly lifted application 

键入组合器

翻译显示了我们使用组合器的方式,这给我们提供了关于它们的types应该是什么的一个线索。 UP只是设置构造函数,所以,写入未翻译的types,并允许Pi的“Agda符号”,我们应该

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

K组合器用于将某个typesA的值提升到某个其他typesG的常数函数。

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

S组合器用于将应用程序提升到所有零件可能依赖的types上。

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

如果你看看S的types,你会发现它正确地说明了types理论的情境化应用规则,所以这就是反映应用结构的合适之处。 这是它的工作!

然后,我们只适用于封闭的东西

  f : Pi AB a : A -------------- fa : B a 

但是有一个障碍。 我在普通types理论中写了组合型的types,而不是组合型理论。 幸运的是,我有一台机器可以进行翻译。

组合式系统

 --------- 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 : AB : U ----------------- A ={norm} B M : B 

所以你有它,在它所有的不可读的荣耀:一套组合的介绍Set:Set

还有一点问题。 系统的语法不能为S猜测GAB参数,对于K也是如此。 相应地,我们可以通过algorithmvalidation打字派生 ,但是我们不能像原始系统那样仅仅检验组合项。 可能的工作是要求types检查者的input对S和K的使用进行types注释,有效地logging派生。 但那是另一种蠕虫

如果你足够敏锐,那么这是一个停下来的好地方。 其余的是“幕后”的东西。

生成组合器的types

我使用相关types理论术语中的括号抽象翻译生成了这些组合types。 为了说明我是如何做到的,并且使这个post不完全没有意义,让我提供我的设备。

我可以编写组合器的types,完全抽象其参数,如下所示。 我使用了便捷的pil函数,它结合了Pi和lambda来避免重复域types,而且有助于我使用Haskell的函数空间来绑定variables。 也许你几乎可以阅读以下内容!

 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) 

有了这些定义,我提取了相关的开放子项,并通过翻译运行。

德Bruijn编码工具包

以下是如何build立pil 。 首先,我定义了一类Fin ite集,用于variables。 每个这样的集合都有一个构造函数保存到上面的集合中,再加上一个新的top元素,你可以把它们区分开来: embd函数告诉你一个值是否在emb的图像中。

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

当然,我们可以将Fin for ZeSuc实例化

 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 xy where wk :: x -> y 

wk函数应该把x的元素作为y最大元素embedded,这样y中的额外的东西就更小了,因此在de Bruijn指数术语中,更局部的绑定了。

 instance Fin y => Le Ze y where wk = magic -- nothing to embed instance Le xy => 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级的skullduggery。

 lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x lam sf = 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 sf = Pi s (lam sf) 

高阶函数并不只是给你一个表示variables的术语,而是给你一个重载的东西,在variables可见的任何范围内变成variables的正确表示。 也就是说,我按照types区分不同范围的麻烦,给了Haskell types检查器足够的信息来计算de Bruijn表示的翻译所需的移位。 为什么养一只狗,吠叫自己?

我想在某些情况下,“支架抽象”也适用于依赖types。 在下面的文章的第5部分中,您会发现一些K和Stypes:

离奇但意义重大的巧合
依赖types安全的语法和评估
Conro McBride,斯特拉斯克莱德大学,2010年

将lambdaexpression式转换为组合expression式大致对应于将自然演绎certificate转换为希尔伯特样式certificate。