直觉型理论的组合逻辑等价物是什么？ [英] What is the combinatory logic equivalent of intuitionistic type theory?

查看：174 发布时间：2018/4/18 15:35:42 haskell types functional-programming logic agda

本文介绍了直觉型理论的组合逻辑等价物是什么？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

最近我完成了一门以Haskell和Agda（一种依赖类型的函数式编程语言）为特色的大学课程，并想知道是否可以用组合逻辑来替代这些中的lambda演算。对于Haskell来说，使用S和K组合器似乎是可能的，从而使它没有任何问题。我想知道Agda的等价物是什么。也就是说，我们可以制作一个与Agda等价的相关类型函数式编程语言而不使用任何变量吗？

另外，是否有可能用组合器代替量化？我不知道这是否是巧合，但是例如通用量化使得类型签名看起来像一个lambda表达式。有没有办法从类型签名中去除通用量化而不改变其含义？例如。 in：

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

同样的事情可以在不使用任何形式的情况下表达吗？
<解决方案

所以我想了一下，取得了一些进展。这是第一次以Martin-Löf简单（但不一致）的 Set：Set 系统以组合形式编码的第一步。这不是一个好的完成方式，但它是最容易入门的地方。这种类型理论的语法只是带有类型注释的lambda-演算，Pi类型和一个Universe Set。

目标类型理论

为了完整起见，我将介绍规则。上下文有效性只是说你可以通过邻接 Set s的新变量从空构建上下文。

  G |  - 有效G |  -  S：设置
 ------------ -  ----------------------------- x新鲜G 
。 |  - 有效的G，x：S |  - 有效的

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

  G |  - 有效G |  -  S：设置G |  -  T：Pi S \ x：S  - >设置
 ------------------ --------------------------- ------------------ 
 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 |  - 有效G |  -  s：SG |  -  T：设置
 ------------- -  x：S in G ----------------------------- S = {beta} T 
 G |  -  x： SG |  -  s：T

绑定运算符，因此Pi的第二个参数应该是计算返回类型依赖于输入的方式的函数。按照惯例（例如在Agda中，但遗憾的是不在Haskell中），lambda的范围尽可能地向右延伸，所以当它们是高阶操作符的最后一个参数时，通常可以将其抽象化为无瑕疵：您可以看到我做了与皮。您的Agda类型（x：S） - > T 变成 Pi S \ x：S - > T 。

（ Digression 。如果您希望能够合成抽象类型如果您切换到检查作为您的工作方式，您仍然需要注释来检查beta-redex，如（\ x - > t）s ，因为你无法从整体上猜测零件的类型，所以建议现代设计师检查类型并从句法中排除beta-redexes。）

（ Digression 。此系统不一致为 Set：Set 允许编码当Martin-Löf提出这个理论的时候，Girard在他自己的不一致的System U中给了他一个编码。由于Hurkens，后来的悖论是我们所知道的最有毒的结构。）

Combinator语法和规范化

无论如何，我们有两个额外的符号Pi和Set，所以我们也许可以用S来管理一个组合的转换， K a再加上两个额外的符号：我选择U代表宇宙，P代表产品。

现在我们可以定义无类型的组合语法（带有自由变量）：

  data SKUP = S | K | U | P导出（Show，Eq）
 
数据Unty a 
 = C SKUP 
 | Unty a：。 Unty 
 | V a 
导出（Functor，Eq）
 infixl 4：。

请注意，我已经包含了包含由类型表示的自由变量的方法。在这个语法中一个。除了作为我的反射（每一个值得名称的语法都是一个有 return 嵌入变量和>> = perfoming substitution），它可以很方便地表示将转换条件转换为绑定到它们的组合形式的过程中的中间阶段。

这里是规范化：

  norm :: Unty a  - > Unty是
范数（f：.a）=范数f $。 a 
规范c = c 
 
（$。）:: Unty a  - > Unty a  - > Unty a  - 以正常形式需要第一个参数
 C S：。 F ：。一美元。 g = f $。 g $。 （a：g） -  S f a g = f g（a g）共享环境
 C K：。一美元。 g = a  -  K a g =下降环境
 n $。 g = n：。规范g  - 以正常形式保证产出
 infixl 4 $。

（读者的练习是定义一个完全正常形式的类型并锐化这些操作。）

表示类型理论

现在我们可以为我们的类型理论定义一种语法。 p>

  data Tm a 
 = Var a 
 | Lam（Tm a）（Tm（Su a）） -  Lam是绑定发生的唯一地方
 | Tm a：$ Tm a 
 | Pi（Tm a）（Tm a） -  Pi的第二个参数是计算Set 
 |的函数设置
 deriving（Show，Functor）
 infixl 4：$ 
 
数据Ze 
 magic :: Ze  - > 
 magic x = x`seq`错误悲剧！ 
 
数据Su a = Ze | Su a derived（Show，Functor，Eq）

我在Bellegarde中使用de Bruijn索引表示法，挂钩方式（如Bird和Paterson推广）。类型 Su a 比 a 多一个元素，我们用它作为活页夹下自由变量的类型， Ze 作为新绑定变量， Su x 是旧自由变量<$ c $的移位表示c> x 。

翻译术语到组合器

我们根据括号抽象得到了通常的翻译。

  tm :: Tm a  - > （a）= b $ b tm（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  - 绑定一个变量，构建一个函数
 bra（V Ze）= C S：。 C K：。 C K  - 变量本身产生身份
 bra（V（Su x））= C K：。 V x  - 自由变量变成常量
 bra（C c）= C K：。 C c  -  combinators变成常数
 bra（f：。a）= C S：。胸罩f：。 bra a  -  S正好取消应用程序

输入组合符号

该翻译显示了我们使用组合器的方式，这让我们知道它们的类型应该是什么。 U 和 P 只是设置的构造函数，所以，编写未翻译的类型并允许Pi使用Agda notation有：

U：Set P：（A：Set） - > （B：（a：A）→> Set）→>设置
K 组合子用于提升某些类型 A 的值与其他类型的 G 。
G：Set A：Set ------------------------ ------- K：（a：A） - > （g：G）→> A
S 组合子用于提升
G：设置 A：（g： G） - >设置 B：（g：G） - > （a：A g） - >设置 --------------------------------------------- （f：（g：G） - >（a：A g）→> B ga）→> （a：（g：G） - > A g） - > （g：G） - > B g（ag）
如果您查看 S ，你会发现它正好说明了类型理论的 contextualised 应用程序规则，所以这就是反映应用程序结构的适用条件。这是它的工作！
然后，我们只有应用程序关闭的东西 f：Pi AB a：A -------------- fa：B a 但是有一个障碍。我用普通类型理论写出了组合型的类型，而不是组合型理论。幸运的是，我有一台机器可以进行翻译。一个组合类型系统 --------- U：U --------------------- ------------------------------------ P：PU（S（S（KP）（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 （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）（S（S（KS）（KK））（KK））））（S（S（KP）（S（S（KP）（K [G]））（ S（S（KS）（K（KK）（K [A]）））（S（S（KS）（KK））（KK）））））（S（KS）（S（KK）（KP）））（S（KK）（K [G]））））（S（S（KS）（S（KK）（KS）））（S（S（KS）））（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）（（S（S（KS）（KK））（S（SK（KS））（S（S（KS）（S（KK）（KK））））（S（KK）（KK））））））） M：AB：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  - >设置
 
 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  - > $ _ $ 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）
  
通过这些定义， em>打开子项并通过翻译运行。
 
 $ b  de Bruijn编码工具包
 
 
 以下是如何建立 pil 。首先，我定义了一个 Fin  ite集，用于变量。每个这样的集合都有一个构造函数 - 保存 emb 到上面的集合中，再加上一个新的 top 元素，你可以告诉他们： embd 函数告诉你一个值是否在 emb 的图像中。
  class Fin x其中
 top :: Su x 
 emb :: x  - > Su x 
 embd :: Su x  - >也许x 
  
当然，我们可以实例化 Fin  for  Ze 和 Suc

实例Fin Ze其中 top = Ze - Ze是唯一的，所以最高的 emb = magic embd _ = Nothing - 没有什么可以嵌入实例Fin x => Fin（Su x）其中 top = Su top - 最高的是一个更高的 emb Ze = Ze - emb保留Ze emb（Su x）= Su（emb x） - - 和Su embd Ze = Just Ze - Ze绝对嵌入 embd（Su x）= fmap Su（embd x） - 否则，等着看弱化操作来定义低于或等于。 class（Fin x，Fin y）=> Le x y其中 wk :: x - > y wk 函数应该嵌入元素 x 作为 y 中最大的元素，这样< c $ c> y 较小，因此de Bruijn指数术语更局部地绑定。实例Fin y => Le Ze y其中 wk = magic - 无法嵌入实例Le x y => Le（Su x）（Su y）其中 wk x =案例x的 Nothing - >顶部 - 顶部地图顶部只是y - > emb（wk y） - 嵌入式获得减弱和嵌入一旦你完成了整理，其中有一部分是n级头骨。 Tm x - > （（全部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 - > （（全部y Le（Su x）y => Tm y） - > Tm（Su x）） - > Tm x pil sf = Pi s（lam sf）

高阶函数不会只是给你一个表示变量的术语，它会给你一个 overloaded 的东西，这个东西在变量可见的任何范围内变成变量的正确表示。也就是说，我按照类型区分不同范围的问题给了Haskell类型检查器足够的信息来计算转换为de Bruijn表示所需的移位。为什么养狗和吠叫自己？

I recently completed a university course which featured Haskell and Agda (a dependent typed functional programming language), and was wondering if it was possible to replace lambda calculus in these with combinatory logic. With Haskell this seems possible using the S and K combinators, thus making it point-free. I was wondering what the equivalent was for Agda. I.e., can one make a dependently typed functional programming language equivalent to Agda without using any variables?

Also, is it possible to somehow replace quantification with combinators? I don't know if this is a coincidence but universal quantification for example makes a type signature look like a lambda expression. Is there a way to remove universal quantification from a type signature without changing its meaning? E.g. in:
forall a : Int -> a < 0 -> a + a < a
Can the same thing be expressed without using a forall?
解决方案
So I thought about it a bit more and made some progress. Here's a first stab at encoding Martin-Löf's delightfully simple (but inconsistent) Set : Set system in a combinatory style. It's not a good way to finish, but it's the easiest place to get started. The syntax of this type theory is just lambda-calculus with type annotations, Pi-types, and a universe Set.

The Target Type Theory

For completeness' sake, I'll present the rules. Context validity just says you can build contexts from empty by adjoining fresh variables inhabiting Sets.
G |- valid G |- S : Set -------------- ----------------------------- x fresh for G . |- valid G, x:S |- valid
And now we can say how to synthesize types for terms in any given context, and how to change the type of something up to the computational behaviour of the terms it contains.
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
In a small variation from the original, I've made lambda the only binding operator, so the second argument of Pi should be a function computing the way the return type depends on the input. By convention (e.g. in Agda, but sadly not in Haskell), scope of lambda extends rightwards as far as possible, so you can often leave abstractions unbracketed when they're the last argument of a higher-order operator: you can see I did that with Pi. Your Agda type (x : S) -> T becomes Pi S \ x:S -> T.

(Digression. Type annotations on lambda are necessary if you want to be able to synthesize the type of abstractions. If you switch to type checking as your modus operandi, you still need annotations to check a beta-redex like (\ x -> t) s, as you have no way to guess the types of the parts from that of the whole. I advise modern designers to check types and exclude beta-redexes from the very syntax.)

(Digression. This system is inconsistent as Set:Set allows the encoding of a variety of "liar paradoxes". When Martin-Löf proposed this theory, Girard sent him an encoding of it in his own inconsistent System U. The subsequent paradox due to Hurkens is the neatest toxic construction we know.)

Combinator Syntax and Normalization

Anyhow, we have two extra symbols, Pi and Set, so we might perhaps manage a combinatory translation with S, K and two extra symbols: I chose U for the universe and P for the product.

Now we can define the untyped combinatory syntax (with free 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 :.
Note that I've included the means to include free variables represented by type a in this syntax. Apart from being a reflex on my part (every syntax worthy of the name is a free monad with return embedding variables and >>= perfoming substitution), it'll be handy to represent intermediate stages in the process of converting terms with binding to their combinatory form.

Here's normalization:
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 $.
(An exercise for the reader is to define a type for exactly the normal forms and sharpen the types of these operations.)

Representing Type Theory

We can now define a syntax for our type theory.
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)
I use a de Bruijn index representation in the Bellegarde and Hook manner (as popularised by Bird and Paterson). The type Su a has one more element than a, and we use it as the type of free variables under a binder, with Ze as the newly bound variable and Su x being the shifted representation of the old free variable x.

Translating Terms to Combinators

And with that done, we acquire the usual translation, based on bracket abstraction.
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

Typing the Combinators

The translation shows the way we use the combinators, which gives us quite a clue about what their types should be. U and P are just set constructors, so, writing untranslated types and allowing "Agda notation" for Pi, we should have
U : Set P : (A : Set) -> (B : (a : A) -> Set) -> Set
The K combinator is used to lift a value of some type A to a constant function over some other type G.
G : Set A : Set ------------------------------- K : (a : A) -> (g : G) -> A
The S combinator is used to lift applications over a type, upon which all of the parts may depend.
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)
If you look at the type of S, you'll see that it exactly states the contextualised application rule of the type theory, so that's what makes it suitable to reflect the application construct. That's its job!

We then have application only for closed things
f : Pi A B a : A -------------- f a : B a
But there's a snag. I've written the types of the combinators in ordinary type theory, not combinatory type theory. Fortunately, I have a machine that will make the translation.

A Combinatory Type System

--------- 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
So there you have it, in all its unreadable glory: a combinatory presentation of Set:Set!

There's still a bit of a problem. The syntax of the system gives you no way to guess the G, A and B parameters for S and similarly for K, just from the terms. Correspondingly, we can verify typing derivations algorithmically, but we can't just typecheck combinator terms as we could with the original system. What might work is to require the input to the typechecker to bear type annotations on uses of S and K, effectively recording the derivation. But that's another can of worms...

This is a good place to stop, if you've been keen enough to start. The rest is "behind the scenes" stuff.

Generating the Types of the Combinators

I generated those combinatory types using the bracket abstraction translation from the relevant type theory terms. To show how I did it, and make this post not entirely pointless, let me offer my equipment.

I can write the types of the combinators, fully abstracted over their parameters, as follows. I make use of my handy pil function, which combines Pi and lambda to avoid repeating the domain type, and rather helpfully allows me to use Haskell's function space to bind variables. Perhaps you can almost read the following!
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)
With these defined, I extracted the relevant open subterms and ran them through the translation.

A de Bruijn Encoding Toolkit

Here's how to build pil. Firstly, I define a class of Finite sets, used for variables. Every such set has a constructor-preserving embedding into the set above, plus a new top element, and you can tell them apart: the embd function tells you if a value is in the image of emb.
class Fin x where top :: Su x emb :: x -> Su x embd :: Su x -> Maybe x
We can, of course, instantiate Fin for Ze and 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
Now I can define less-or-equals, with a weakening operation.
class (Fin x, Fin y) => Le x y where wk :: x -> y
The wk function should embed the elements of x as the largest elements of y, so that the extra things in y are smaller, and thus in de Bruijn index terms, bound more locally.
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
And once you've got that sorted out, a bit of rank-n skullduggery does the rest.
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)
The higher-order function doesn't just give you a term representing the variable, it gives you an overloaded thing which becomes the correct representation of the variable in any scope where the variable is visible. That is, the fact that I go to the trouble of distinguishing the different scopes by type gives the Haskell typechecker enough information to compute the shifting required for the translation to de Bruijn representation. Why keep a dog and bark yourself?

这篇关于直觉型理论的组合逻辑等价物是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文

直觉型理论的组合逻辑等价物是什么？ [英] What is the combinatory logic equivalent of intuitionistic type theory?

问题描述

目标类型理论

Combinator语法和规范化

表示类型理论

翻译术语到组合器

一个组合类型系统

生成组合类型

de Bruijn编码工具包

The Target Type Theory

Combinator Syntax and Normalization

Representing Type Theory

Translating Terms to Combinators

Typing the Combinators

A Combinatory Type System

Generating the Types of the Combinators

A de Bruijn Encoding Toolkit

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

直觉型理论的组合逻辑等价物是什么？ [英] What is the combinatory logic equivalent of intuitionistic type theory?

问题描述

目标类型理论

Combinator语法和规范化

表示类型理论

翻译术语到组合器

一个组合类型系统

生成组合类型

de Bruijn编码工具包

The Target Type Theory

Combinator Syntax and Normalization

Representing Type Theory

Translating Terms to Combinators

Typing the Combinators

A Combinatory Type System

Generating the Types of the Combinators

A de Bruijn Encoding Toolkit

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭