Skip to content
This repository has been archived by the owner on Feb 8, 2022. It is now read-only.

Remove asCommutativeRing from Heyting #94

Merged
merged 2 commits into from
Oct 14, 2015
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,9 @@ lazy val aggregate = project.in(file("."))
lazy val core = crossProject.crossType(CrossType.Pure)
.settings(moduleName := "algebra")
.settings(mimaDefaultSettings: _*)
.settings(previousArtifact := Some("org.spire-math" %% "algebra" % "0.3.1"))
// TODO: update this to a published stable version, e.g. 0.4.0
//.settings(previousArtifact := Some("org.spire-math" %% "algebra" % "0.3.1"))
.settings(previousArtifact := None)
.settings(algebraSettings: _*)
.settings(sourceGenerators in Compile <+= (sourceManaged in Compile).map(Boilerplate.gen))

Expand Down
24 changes: 19 additions & 5 deletions core/src/main/scala/algebra/lattice/Bool.scala
Original file line number Diff line number Diff line change
@@ -1,31 +1,45 @@
package algebra
package lattice

import ring.CommutativeRing
import scala.{specialized => sp}

/**
* Boolean algebras are Heyting algebras with the additional
* constraint that the law of the excluded middle is true
* (equivalently, double-negation is true).
*
*
* This means that in addition to the laws Heyting algebras obey,
* boolean algebras also obey the following:
*
*
* - (a ∨ ¬a) = 1
* - ¬¬a = a
*
*
* Boolean algebras generalize classical logic: one is equivalent to
* "true" and zero is equivalent to "false". Boolean algebras provide
* additional logical operators such as `xor`, `nand`, `nor`, and
* `nxor` which are commonly used.
*
*
* Every boolean algebras has a dual algebra, which involves reversing
* true/false as well as and/or.
*/
trait Bool[@sp(Int, Long) A] extends Any with Heyting[A] {
trait Bool[@sp(Int, Long) A] extends Any with Heyting[A] { self =>
def imp(a: A, b: A): A = or(complement(a), b)

def dual: Bool[A] = new DualBool(this)
/**
* Every Boolean algebra is a CommutativeRing, but we don't extend
* CommutativeRing because, e.g. we might want a Bool[Int] and CommutativeRing[Int] to
* refer to different structures, by default.
*/
def asCommutativeRing: CommutativeRing[A] =
new CommutativeRing[A] {
def zero: A = self.zero
def one: A = self.one
def plus(x: A, y: A): A = self.xor(x, y)
def negate(x: A): A = self.complement(x)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

negate here is still broken. It should be

def negate(x: A): A = x

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aha, right. I'll fix that now. Thanks!

def times(x: A, y: A): A = self.and(x, y)
}
}

class DualBool[@sp(Int, Long) A](orig: Bool[A]) extends Bool[A] {
Expand Down
27 changes: 8 additions & 19 deletions core/src/main/scala/algebra/lattice/Heyting.scala
Original file line number Diff line number Diff line change
@@ -1,41 +1,39 @@
package algebra
package lattice

import ring.CommutativeRing

import scala.{specialized => sp}

/**
* Heyting algebras are bounded lattices that are also equipped with
* an additional binary operation `imp` (for impliciation, also
* written as →).
*
*
* Implication obeys the following laws:
*
*
* - a → a = 1
* - a ∧ (a → b) = a ∧ b
* - b ∧ (a → b) = b
* - a → (b ∧ c) = (a → b) ∧ (a → c)
*
*
* In heyting algebras, `and` is equivalent to `meet` and `or` is
* equivalent to `join`; both methods are available.
*
*
* Heyting algebra also define `complement` operation (sometimes
* written as ¬a). The complement of `a` is equivalent to `(a → 0)`,
* and the following laws hold:
*
*
* - a ∧ ¬a = 0
*
*
* 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
* `Bool`.
*/
trait Heyting[@sp(Int, Long) A] extends Any with BoundedLattice[A] { self =>
trait Heyting[@sp(Int, Long) A] extends Any with BoundedLattice[A] {
def and(a: A, b: A): A
def meet(a: A, b: A): A = and(a, b)

Expand All @@ -49,15 +47,6 @@ trait Heyting[@sp(Int, Long) A] extends Any with BoundedLattice[A] { self =>
def nand(a: A, b: A): A = complement(and(a, b))
def nor(a: A, b: A): A = complement(or(a, b))
def nxor(a: A, b: A): A = complement(xor(a, b))

def asCommutativeRing: CommutativeRing[A] =
new CommutativeRing[A] {
def zero: A = self.zero
def one: A = self.one
def plus(x: A, y: A): A = self.xor(x, y)
def negate(x: A): A = self.complement(x)
def times(x: A, y: A): A = self.and(x, y)
}
}

trait HeytingFunctions {
Expand Down