Innovenergy_trunk/frontend/node_modules/fp-ts/es6/HeytingAlgebra.d.ts

33 lines
1.2 KiB
TypeScript
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/**
* Heyting algebras are bounded (distributive) lattices that are also equipped with an additional binary operation
* `implies` (also written as `→`). Heyting algebras also define a complement operation `not` (sometimes written as
* `¬a`)
*
* However, in Heyting algebras this operation is only a pseudo-complement, since Heyting algebras do not necessarily
* provide the law of the excluded middle. This means that there is no guarantee that `a ¬a = 1`.
*
* Heyting algebras model intuitionistic logic. For a model of classical logic, see the boolean algebra type class
* implemented as `BooleanAlgebra`.
*
* A `HeytingAlgebra` must satisfy the following laws in addition to `BoundedDistributiveLattice` laws:
*
* - Implication:
* - `a → a <-> 1`
* - `a ∧ (a → b) <-> a ∧ b`
* - `b ∧ (a → b) <-> b`
* - `a → (b ∧ c) <-> (a → b) ∧ (a → c)`
* - Complemented
* - `¬a <-> a → 0`
*
* @since 2.0.0
*/
import { BoundedDistributiveLattice } from './BoundedDistributiveLattice'
/**
* @category model
* @since 2.0.0
*/
export interface HeytingAlgebra<A> extends BoundedDistributiveLattice<A> {
readonly implies: (x: A, y: A) => A
readonly not: (x: A) => A
}