代码之家 › 专栏 › 技术社区 › TomR

什么是Coq函数定义'definition Term:=for all T:Type,Term T.'的意思?

coq logic functional-programming

TomR · 技术社区 · 6 年前

Definition Term := forall T:Type,  term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)

为什么我们需要 福尔 函数定义中的结构,它给出了什么附加意义?是否正在创建某种集合-即-该函数返回一组结果-每种类型一个结果?

我在看书 http://adam.chlipala.net/cpdt/cpdt.pdf “第十二章宇宙与公理”,这个问题是我之前问题的延续 How to understand Coq type constructor var (t: T)

1 回复 | 直到 6 年前

Li-yao Xia 6 年前

在参数HOAS中,参数 T 表示术语中可能出现的变量集。例如,如果希望术语最多使用两个变量,则它可能具有 term bool bool 有两个居民。因此,一个封闭项(没有自由变量)可以天真地被类型化 term void ,其中 void 是空类型:

Inductive void := .

结果是相当于 forall A, term A forall A, void -> A 在一个方向,只在另一个方向专攻)。后一种封闭项的表示更便于嵌入到其他开放项中。

推荐文章

Amit Saha · Java Stream iterate在检查奇偶时不使用谓词

2 年前

nanounanue · 使用python和高级操作符的函数管道

6 年前

Zazaeil · 这个特定的递归可以用尾部优化的方式重写吗?

6 年前

Ben2209 · 将methodcaller和attrgetter与排序

6 年前

corvid · 使用ramda通过变量进行升序/降序

6 年前

OddDragon · Java8:使用IntStream作为自定义收集器的供应商参数

6 年前

MichaÅ Å rajer · 将int列表折叠到kotlin中的范围列表

6 年前

Saravana Kumar M · 如何使用java 8 streams和lambdas迭代并处理其值为元素列表的映射的值

6 年前

CodingNow · Scala:如何制作多种方法并逐一应用?

6 年前

Saber · 在使用流时,使用多个map()会比在单个map()中聚合所有逻辑花费更多的时间吗?

6 年前