bump dependencies
1 
package algebra 

2 
package lattice 

3  
4 
import scala.{specialized => sp} 

5  
6 
/**


7 
* Heyting algebras are bounded lattices that are also equipped with


8 
* an additional binary operation `imp` (for implication, also


9 
* written as →).


10 
*


11 
* Implication obeys the following laws:


12 
*


13 
*  a → a = 1


14 
*  a ∧ (a → b) = a ∧ b


15 
*  b ∧ (a → b) = b


16 
*  a → (b ∧ c) = (a → b) ∧ (a → c)


17 
*


18 
* In heyting algebras, `and` is equivalent to `meet` and `or` is


19 
* equivalent to `join`; both methods are available.


20 
*


21 
* Heyting algebra also define `complement` operation (sometimes


22 
* written as ¬a). The complement of `a` is equivalent to `(a → 0)`,


23 
* and the following laws hold:


24 
*


25 
*  a ∧ ¬a = 0


26 
*


27 
* However, in Heyting algebras this operation is only a


28 
* pseudocomplement, since Heyting algebras do not necessarily


29 
* provide the law of the excluded middle. This means that there is no


30 
* guarantee that (a ∨ ¬a) = 1.


31 
*


32 
* Heyting algebras model intuitionistic logic. For a model of


33 
* classical logic, see the boolean algebra type class implemented as


34 
* `Bool`.


35 
*/


36 
trait Heyting[@sp(Int, Long) A] extends Any with BoundedDistributiveLattice[A] { self => 

37 
def and(a: A, b: A): A 

38  2 
def meet(a: A, b: A): A = and(a, b) 
39  
40 
def or(a: A, b: A): A 

41  2 
def join(a: A, b: A): A = or(a, b) 
42  
43 
def imp(a: A, b: A): A 

44 
def complement(a: A): A 

45  
46 
def xor(a: A, b: A): A = or(and(a, complement(b)), and(complement(a), b)) 

47 
def nand(a: A, b: A): A = complement(and(a, b)) 

48 
def nor(a: A, b: A): A = complement(or(a, b)) 

49 
def nxor(a: A, b: A): A = complement(xor(a, b)) 

50 
}


51  
52 
trait HeytingGenBoolOverlap[H[A] <: Heyting[A]] { 

53 
def and[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

54 
ev.and(x, y) 

55 
def or[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

56 
ev.or(x, y) 

57 
def xor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

58 
ev.xor(x, y) 

59 
}


60  
61 
trait HeytingFunctions[H[A] <: Heyting[A]] extends 

62 
BoundedMeetSemilatticeFunctions[H] with 

63 
BoundedJoinSemilatticeFunctions[H] { 

64  
65 
def complement[@sp(Int, Long) A](x: A)(implicit ev: H[A]): A = 

66 
ev.complement(x) 

67  
68 
def imp[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

69 
ev.imp(x, y) 

70 
def nor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

71 
ev.nor(x, y) 

72 
def nxor[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

73 
ev.nxor(x, y) 

74 
def nand[@sp(Int, Long) A](x: A, y: A)(implicit ev: H[A]): A = 

75 
ev.nand(x, y) 

76 
}


77  
78  
79 
object Heyting extends HeytingFunctions[Heyting] with HeytingGenBoolOverlap[Heyting] { 

80  
81 
/**


82 
* Access an implicit `Heyting[A]`.


83 
*/


84 
@inline final def apply[@sp(Int, Long) A](implicit ev: Heyting[A]): Heyting[A] = ev 

85 
}

Read our documentation on viewing source code .