Coq中的术语作为类型 [英] Terms as types in Coq

问题描述

Parameter R: Type.
Parameter P: R.
Parameter O: P. (*Error: The term "P" has type "R" which should be Set, Prop or Type.*)

无效，因为术语在Coq中不能包含术语。我们如何绕过这一限制？人们会想到几种可能性：参数化，子集类型，类，记录，合奏，明确的宇宙层次...我的问题是关于将术语作为Coq中的类型实现的推荐和最简单的方法（以及MWE）。 PS。我不认为推荐和最简单是一致的。

doesn't work because terms can't have terms in Coq. How can we bypass this restriction? One would imagine several possibilities: parametrization, subset types, classes, records, ensembles, explicit universe levels... My question is about the recommended and easiest way(s) of implementing terms as types in Coq (along w/ MWEs). PS. I don't assume the "recommended" and "easiest" to coincide.

一个简单的例子是

Parameter Obj: Type.
Parameter Phy Int: Obj. (*physical, intelligent*)
Parameter tree house: Phy.

推荐答案

基于建议和随后的半反驳的答案@ejgallego：

An answer based on a suggestion and subsequent semi-refutation @ejgallego:

Let Obj := Type.
Let Phy:Obj := Type.
Let tree:Phy := Type.
Parameter house branch leaf: Phy.  
Let oak:tree := Type.
Let moldyoak:oak := Type.
Parameter moldyoak1:moldyoak.
Parameter moldyoak11:moldyoak1.

解决方案是一致的，但并不合理：

The solution is consistent but unsound:

Check nat:moldyoak. (*(nat:moldyoak) : moldyoak*)

所以我们正在寻找另一个

So we're looking for another one

这篇关于Coq中的术语作为类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！