【coq】函数语言设计笔记 11

Relations
Basic Properties
Reflexive, Transitive Closure

relation properties 关系的性质

Relation
A binary relation on a set X is a family of propositions parameterized by two elements of X – i.e., a proposition about pairs of elements of X.
集合 X 上的二元*'关系（Relation）'* 指所有由两个 X 中的元素参数化的命题，即，有关一对 X 中的元素的命题。
Coq 标准库中的“关系” 单指“某个集合中的元素之间二元关系”

基本性质

偏函数
对于集合 X 上的关系 R ，如果对于任何 x 最多只有一个 y 使得 R x y 成立 – 即，R x y1 和 R x y2 同时成立蕴含 y1 = y2 ，则称 R 为*'偏函数'* 。

举例

然而，数值上的 ≤ 关系并不是个偏函数。
据其定义我们有 0 ≤ 0 和 0 ≤ 1 ，这样会推出 0 = 1 。这是不可能的
证明：

自反关系
集合 X 上的*'自反关系'* 是指 X 的每个元素都与其自身相关。

传递关系
如果 R a b 和 R b c 成立时 R a c 也成立，则称 R 为*'传递关系'* 。

对称关系
如果 R a b 蕴含 R b a，那么 R 就是*'对称关系'* 。

反对称关系
如果 R a b 和 R b a 成立时有 a = b ，那么 R 就是 ' 反对称关系 ' 。

等价关系
如果一个关系满足自反性、对称性和传递性，那么它就是*'等价关系'* 。

偏序关系
自反性、反对称性和传递性

预序关系
自反性、传递性

自反传递闭包

关系 R 的*'自反传递闭包'* 是最小的包含 R 的自反传递关系。

常用

coq 中的定义：
它直接将自反传递闭包定义为“包含 R 的，同时满足自反性和传递性的最小的关系”

然而此定义对于证明来说不是很方便，因为 rt_trans 的“非确定性” 有时会让归纳变得很棘手。

其他阅读；
集合论—关系的自反、对称和传递闭包

来自 < https://blog.csdn.net/baishuiniyaonulia/article/details/93231859 >

【coq】函数语言设计笔记 11 - rel相关推荐

【历史上的今天】6 月 5 日：洛夫莱斯和巴贝奇相遇；公钥密码学先驱诞生；函数语言设计先驱出生
整理 | 王启隆透过「历史上的今天」,从过去看未来,从现在亦可以改变未来. 今天是 2022 年 6 月 5 日,世界环境日.1972 年 6 月 5 日至 16 日,联合国人类环境会议在斯德哥尔摩 ...
[C++程序语言设计笔记一]面向对象编程抽象，继承，重写基本介绍
今天是个不错的日子,不仅有人收了我做徒弟从此传授我有关C++的一些知识,由于前一段时间喜欢上了外挂的研究也用到了一些MFC的知识及一些Windows APIs编程,但是对C++还是没有从根本上认识.我 ...
C语言学习笔记06-占位符格式、C基本类型及逃逸字符一些细节（附介绍BCD码）
主要整理有关占位符格式与逃逸字符的一些细节朋友们,看栗子--"BCD解码" (文末附BCD码介绍) 一个BCD数的十六进制是0x12(对应二进制表示:0001 0010),它表达 ...
c语言中void arrout,c语言学习笔记(数组、函数
<c语言学习笔记(数组.函数>由会员分享,可在线阅读,更多相关<c语言学习笔记(数组.函数(53页珍藏版)>请在人人文库网上搜索. 1.数组2010-3-29 22:40一维数 ...
r语言c函数怎么用,R语言学习笔记——C#中如何使用R语言setwd()函数
在R语言编译器中,设置当前工作文件夹可以用setwd()函数. > setwd("e://桌面//") > setwd("e:\桌面\") > ...
c 语言filter过滤方法,R语言日常笔记（1）filter函数
R语言日常笔记(1)filter函数在处理数据时,过滤数据是最基本的操作之一. 如果想删除一部分无效或者根本不感兴趣的数据. dplyr有filter()函数来做这样的过滤. 使用dplyr,可以帮 ...
9. 设计二个函数分别计算sinx和cosx_从并发模型看 Go 的语言设计
传统的程序语言设计都不会将输入输出作为语言的核心,但 Tony Hoare 认为输入输出是基本的编程原语,且通信顺序进程(Communicating sequential processes,CSP) ...
java语言基础笔记——语句，函数
java语言基础笔记语句判断结构(重点) 三种格式: 第一种: if(条件表达式){ 执行语句; } System.out.println(); 举例: int a ...
C语言基础之11：字符串和字符串函数
Tips1: 函数:gets().gets_s().fgets().puts().fputs().strcat().strncat(). strcmp().strncmp().strcpy().str ...
C 语言的可变参数表函数的设计
首先在介绍可变参数表函数的设计之前,我们先来介绍一下最经典的可变参数表printf函数的实现原理. 一.printf函数的实现原理在C/C++中,对函数参数的扫描是从后向前的.C/C++的函数参数是 ...

【coq】函数语言设计笔记 11 - rel

【coq】函数语言设计笔记 11 - rel相关推荐

最新文章

热门文章

【coq】函数语言设计 笔记 11 - rel

【coq】函数语言设计 笔记 11 - rel相关推荐

最新文章

热门文章

【coq】函数语言设计笔记 11 - rel

【coq】函数语言设计笔记 11 - rel相关推荐