严格弱序


类别: 函子	组件类型: 概念

描述

严格弱序是一个二元谓词，用于比较两个对象，并返回true如果第一个对象先于第二个对象。此谓词必须满足严格弱序的标准数学定义。下面列出了精确的要求，但它们大致的意思是，严格弱序必须像“小于”一样工作：如果a小于b那么bba不小于a小于ba，如果b小于b那么a小于b小于

c，依此类推。

二元谓词的细化

关联类型

第一个参数类型	严格弱序的第一个参数的类型。
第二个参数类型	严格弱序的第二个参数的类型。第一个参数类型和第二个参数类型必须相同。
结果类型	调用严格弱序时返回的类型。结果类型必须可转换为`bool`.

符号

`F`	严格弱序模型的类型
`X`	严格弱序参数的类型。
`f`	类型为`F`
`x`, `y`, `z`	类型为`X`

定义

两个对象xa，如果y如果两者都为f(x, y)a，如果f(y, x)为假，则称为等价的。请注意，一个对象总是（根据自反性不变式）等价于自身。

有效表达式

除了二元谓词要求中定义的表达式之外，没有其他表达式。

表达式语义

名称	表达式	前置条件	语义	后置条件
函数调用	`f(x, y)`	有序对`(x,y)`在`f`	返回`true`如果`x`x`y`先于`y，否则返回`false	结果为`true`true`y，否则返回`

或

复杂度保证

不变量	`自反性`f(x, x)`y，否则返回`.
必须为	`f(x, y)`反称性`f(x, y)`
暗示	`f(x, y)`a，如果`!f(y, x)`传递性`f(x, y)`.
和	f(y, z)`x`暗示`y`a，如果`y`暗示`z`f(x, z)`x`暗示`z`等价关系的传递性

等价（如上定义）是传递的：如果

x
等价于
y
并且

y

等价于

z，那么

x, 等价于z。（这意味着等价关系实际上满足等价关系的数学定义。）[1]

模型 less<int>