直觉型理论的组合逻辑等价物是什么？
我最近完成了一门以Haskell和Agda（一种依赖类型的函数式编程语言）为特色的大学课程，并想知道是否可以用组合逻辑来替代这些中的lambda演算。 对于Haskell来说，使用S和K组合器似乎是可能的，从而使它没有任何问题。 我想知道Agda的等价物是什么。 也就是说，是否可以使用与Agda等效的独立类型函数式编程语言而不使用任何变量？
另外，是否有可能用组合器取代量化？ 我不知道这是否是巧合，但是例如通用量化使得类型签名看起来像一个lambda表达式。 有没有办法从类型签名中去除通用量化而不改变其含义？ 例如：
forall a : Int -> a < 0 -> a + a < a
同样的事情可以表达而不用使用吗？
所以我想了一下，取得了一些进展。 这是Martin-Löf以组合方式编码的令人愉快的简单（但不一致） Set : Set系统的第一次尝试。 这不是一个好的完成方式，但它是最容易入门的地方。 这种类型理论的语法只是带有类型注释的lambda-calculus，Pi类型和一个Universe Set。
目标类型理论
为了完整起见，我会提出规则。 上下文有效性只是说你可以通过邻接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的第二个参数应该是计算返回类型依赖于输入的函数的函数。 按照惯例（例如，在Agda中，但遗憾的是不在Haskell中），lambda范围尽可能向右延伸，所以当它们是高阶运算符的最后一个参数时，通常可以将抽象区分开来：您可以看到我做了与皮。 你的Agda类型(x : S) -> T变成Pi S x:S -> T
（Digression。如果你希望能够综合抽象类型，那么在lambda上输入注释是必须的，如果你改用类型检查作为你的工作方式，你仍然需要注释来检查beta-redex，例如( x -> t) s ，因为你无法从整体上猜测零件的类型，所以我建议现代设计师检查类型并从句法中排除beta-redex。）
（Digression。这个系统是不一致的，因为Set:Set允许编码各种各样的“说谎者悖论”。当Martin-Löf提出这个理论时，Girard给他发了一个在他自己不一致的System U中的编码。 Hurkens是我们知道的最有毒的建筑。）
组合器语法和规范化
无论如何，我们有两个额外的符号，Pi和Set，所以我们也许可以用S，K和两个额外的符号来管理一个组合的翻译：我选择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在此语法中包含由类型a表示的自由变量的方法。 除了作为我的一个反射（每一个值得名称的语法都是一个带有return嵌入变量的自由monad和>>= perfoming substitution），它可以方便地表示在转换与绑定它们的术语的过程中的中间阶段组合形式。
这是标准化：
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)
我使用贝尔加德和胡克方式的德布鲁恩索引表示法（如Bird和Paterson所普及）。 类型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 combinator用于将应用程序提升到所有零件可能依赖的类型上。
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的组合式演示！
还有一点问题。 系统的语法使您无法为S猜测G ， A和B参数，对于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 EDDING成以上的设置，再加上一个新的top元素，你可以告诉他们分开：在embd函数告诉你，如果一个值是图像中的emb 。
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
当然，我们可以将Fin for 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
现在，我可以定义“不太平等”，并且操作有所减弱。
class (Fin x, Fin y) => Le x y where
wk :: x -> y
该wk功能应嵌入的元素x为最大元素y ，使多余的东西y较小，因而在德布鲁因指数而言，势必更多本地。
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
一旦你把它整理出来，剩下的就是一个排名第一的skullduggery。
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表示所需的移位。 为什么养狗和吠叫自己？
我想在某些情况下，“支架抽象”也适用于依赖类型。 在以下文章的第5部分中，您可以找到一些K和S类型：
离奇但意义重大的巧合
依赖类型安全的语法和评估
Conro McBride，斯特拉斯克莱德大学，2010年
将lambda表达式转换为组合表达式大致对应于将自然演绎证明转换为希尔伯特样式证明。
链接地址: http://www.djcxy.com/p/43343.html上一篇: What is the combinatory logic equivalent of intuitionistic type theory?