实际上是否可能删除“Pi”来自建筑微积分？ [英] Is it actually possible to remove "Pi" from Calculus of Constructions?

问题描述

更简单，更轻松！声明即使没有Pi的存在，编码依赖型系统也是可能的 - 也就是说，您可以重复使用Lam构造函数。但是，如果在某些情况下Pi和Lam的处理方式不同，那又如何呢？

此外，Star可以被删除吗？我认为你可以用λx。x（id）来代替它的所有匹配。 解析方案

code>（a，b）在Haskell中：它既可以是类型也可以是值。您可以对Π和λ使用相同的绑定，typechecker将根据上下文决定您的意思。如果你对另一个绑定进行绑定，那么前者是λ，后者是Π - 这就是为什么你可以用λx明确地取代 * 。 x - 因为之前的资料夹可能是Π，后者是 * code> * 作为活页夹对我没有任何意义）。对于∀=λ和 * =λx有一个更大的问题。 x ：通过传递性 * =∀x。 x ，这是假定 False 的常用方法 - 此类型必须在音响系统中无人居住，因此您不会在所有。

Coq俱乐部最近有一篇关于有趣和有趣的相似之处的帖子（gmane.org给了我没有这样的信息，是我吗？ ），以下是一些摘录：

Dominic Mulligan ：

这里还有一个小书目指向类似的作品：

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf具有讽刺意味的是，根据该文件，Coquand首先提出了带有单一统一活页夹的
结构的微积分，遵循约定
由De Bruijn在AutoMath中创建。

Thorsten Altenkirch：

一个函数和它的类型是非常不同的概念，即使它们有
一些肤浅的语法相似性。

特别是对于新人来说，这个标识非常混乱，
完全误导。我认为应该从他们的意思理解类型
的理论概念，而不是它们的样子。

Andreas Abel ：

我的学生Matthias Benkard也参与过这样的系统，请参阅Type
Checking without类型

http：/ /www.cse.chalmers.se/~abela/benkardThesis.pdf

请注意，第一个系统链接有Π减少（也就是说，您可以像使用lambda表达式一样应用pi类型） - 如果统一Π和λ，您的系统也会拥有它内部（而不是语法上）。第二个链接中描述的系统统一了类型和值。
$ b

一个直接后果是
类型与他们的居民：每一种价值都是一种包含自身
及其所有部分的类型;相反，每种类型都是由其居民组成的复合价值
。

所以实际上只有一个活页夹对于让也许修复）。

The article Simpler, Easier! claims it could be possible to encode dependent type systems even without the presence of "Pi" - that is, you could reuse the "Lam" constructor for it. But how can that be true, if "Pi" and "Lam" are treated differently in some cases?

Moreover, could "Star" be removed? I think you could replace all occurrences of it by "λ x . x" (id).

解决方案

That's just overloading like (a, b) in Haskell: it can be both a type and a value. You can use the same binder for Π and λ and typechecker will decide from the context which one you mean. If you typecheck one binder against another, then the former is λ and the latter is Π — and that's why you can't unambiguously replace * with λ x . x — because then the former binder could be Π and the latter is * (* as a binder doesn't make any sense to me). There is a bigger problem with ∀ = λ and * = λ x . x: by transitivity * = ∀ x . x, which is a common way to postulate False — this type must be uninhabited in a sound system, so you won't have any types at all.

There was a recent thread on Coq-club "Similarities between forall and fun" (gmane.org gives me "No such message", is it just me?), here are some excerpts:

Dominic Mulligan:

And here is another with a small bibliography pointing to similar work:

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf

Ironically, according to that paper Coquand first presented the Calculus of Constructions with a single, unified binder, following a convention established by De Bruijn in AutoMath.

Thorsten Altenkirch:

A function and its type are very different concepts even if they have some superficial syntactic similarity.

Especially for the newcomer this identification is very confusing and completely misleading. I do think that one should understand type theoretical concepts from what they mean and not how they look like.

Andreas Abel:

My student Matthias Benkard also worked on such a system, see "Type Checking without Types"

http://www.cse.chalmers.se/~abela/benkardThesis.pdf

Note that the system described at the first link has Π-reduction (i.e. you can apply pi-types just like lambdas) — your system will have it too, if you unify Π and λ internally (as opposed to syntactically). And the system described at the second link unifies types and values

One immediate consequence is the absence of any distinction between types and their inhabitants: Every value is a type containing itself and all of its parts; and conversely, every type is a composite value consisting of its inhabitants.

so there is really just one binder (except for let and maybe fix).

这篇关于实际上是否可能删除“Pi”来自建筑微积分？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！