case class Function(name: String, degree: Int)
case class Relation(name: String, degree: Int)
We form two kinds of expressions, terms and formulas using these. Both of these are defined recursively.
sealed trait Expression
sealed trait Term extends Expression
sealed trait Formula extends Expression
object Term{
case class Var(name: String) extends Term
case class Const(name: String) extends Term
case class Recursive(function: Function, arguments: Vector[Term]) extends Term{
require(function.degree == arguments.length)
}
}
object Formula{
case class Equality(lhs: Term, rhs: Term) extends Formula
case class Atomic(relation: Relation, arguments: Vector[Term]) extends Formula{
require(relation.degree == arguments.length)
}
case class Or(p: Formula, q: Formula) extends Formula
case class And(p: Formula, q: Formula) extends Formula
case class Implies(p: Formula, q: Formula) extends Formula
case class Equivalent(p: Formula, q: Formula) extends Formula
case class Not(p: Formula) extends Formula
case class ForAll(x: Term.Var, p: Formula) extends Formula
case class Exists(x: Term.Var, p: Formula) extends Formula
}
val sum = Function("+", 2)
val succ = Function("succ", 1)
// Some valid terms
import Term._
val n = Var("n")
val m = Var("m")
val one = Const("1")
Recursive(sum, Vector(n, m))
Recursive(succ, Vector(n))
val two = Recursive(succ, Vector(one))
// An invalid term
import scala.util.Try
val wrong = Try(Recursive(succ, Vector(one, n)))
// Some formulas
import Formula._
val f1 = Equality(one, two)
val f2 = Equality(n, one)
val leq = Relation("<=", 2)
val f3 = Atomic(leq, Vector(one, two))
val f4 = ForAll(n, f2)
val f5 = Exists(n, f2)
val f6 = ForAll(m, f1)
The formulas in mathematical notation are
The language of sets has:
We introduce these as well as a convenience method.
import Term._, Formula._
val phi = Const("empty-set")
val in = Relation("in", 2)
def belongs(x: Term, y: Term) = Formula.Atomic(in, Vector(x, y))
As an example, we define extensionality, i.e. if two sets have the same members, they are equal. $$\forall x\forall y((\forall a\ (a\in x\iff a \in y)) \implies (x = y))$$
val a = Var("a")
def sameMembers(p: Term, q: Term): Formula =
ForAll(a, Equivalent(belongs(a, p), belongs(a, q)))
val x = Var("x")
val y = Var("y")
val extensionality =
ForAll(x,
ForAll(y,
Implies(sameMembers(x, y), Equality(x, y))))
In the language of natural numbers
// Variable in a term
def variables(t: Term): Set[Var] = t match {
case Const(name) => Set()
case Recursive(function, arguments) =>
for{
arg : Term <- arguments.toSet
x <- variables(arg)
} yield x
case Var(name) => Set(Var(name))
}
variables(Recursive(sum, Vector(n, m)))
val p = Recursive(succ, Vector(m))
variables(Recursive(sum, Vector(n, p)))
variables(p)
def freeVariables(fmla: Formula) : Set[Var] = fmla match {
case Equality(lhs, rhs) =>
variables(lhs) union variables(rhs)
case And(p, q) =>
freeVariables(p) union freeVariables(q)
case Implies(p, q) =>
freeVariables(p) union freeVariables(q)
case Equivalent(p, q) =>
freeVariables(p) union freeVariables(q)
case Not(p) =>
freeVariables(p)
case ForAll(x, p) =>
freeVariables(p) - x
case Atomic(relation, arguments) =>
for {
arg: Term <- arguments.toSet
x <- variables(arg)
} yield x
case Exists(x, p) =>
freeVariables(p) - x
case Or(p, q) =>
freeVariables(p) union freeVariables(q)
}
val fmla1 = Exists(x, belongs(x, y))
val fmla2 = ForAll(y, fmla1)
val fmla3 = belongs(x, y)
freeVariables(fmla1)
freeVariables(fmla2)
freeVariables(fmla3)
We have so far:
We also know that we cannot specify sets by arbitrary properties, i.e., like $$\{p : \text{$p$ is a prime}\}$$.
We shall, however, see that we can define sets such as $$\{p \in\mathbb{N} : \text{$p$ is a prime}\}$$ provided we have previously defined (constructed) $\mathbb{N}$.
Let $x$ be a variable. A property of $x$ is a formula $p = p(x)$ so that $p$ has no free variables other than $x$ ($x$ may also not be a free variable).
We cannot define sets with unrestricted comprehension, i.e., of the form $$S = \{x : p(x) \}$$ as we get a paradox with the set $$ S = \{x : x \notin x\}$$
val russell = Not(belongs(x, x))
freeVariables(russell)
Given a set $U$ and a property $p= p(x)$ of the variable $x$, there exists a set $S$ given by $$S = \{x \in U: p(x)\}$$
More formally, fix a formula $p$ with no free variables other than $x$. We have the axiom: $$\forall U\exists S(x\in S \iff (x \in U \land p(x))$$
// we can implement specification for nice properties
val U = (1 to 20).toSet
val S = U.filter(x => x % 3 == 0) // p(x) = x % 3 == 0
show(S)
$A \cup B$ is the set whose elements are elements of $A$ and elements of $B$
Set(1, 3, 4) union Set(3, 7, 9)
The existence of union is given by the axiom of unordered pairs
$$\forall A \forall B\exists C(\forall x\ (x\in C \iff (x\in A \lor x\in B )))$$Given a set of sets $U$, we can take the union of all of these, i.e. there exists $$\bigcup_{A \in U}A$$ such that $x \in \bigcup_{A \in U}A$ if and only if $$\exists A\ (A \in U \land x \in A)$$.
// union of sets
val setOfSets = Set(Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
val bigUnion = setOfSets.flatten
There is an axiom that says $\bigcup_{A \in U}A$ exists (axiom of unions)
val big = Set[Any](Set(1, 2), Set(1, 3), Set(7, 8, 23), Set(7))
big contains (Set(1, 2))
(Set[Any](1, 2)).subsetOf(big)
big contains 1
Set[Any](Set(1, 2)).subsetOf(big)
val anotherBig = Set[Any](1, Set(1), Set(1, 2), Set[Any](2, Set(1, 3)))
anotherBig contains 1
Set[Any](1) subsetOf anotherBig
anotherBig contains Set(1)
import scala.collection.mutable.{Set => mSet}
val ss = mSet[Any](mSet(1), mSet(2))
ss += mSet(3, 4)
ss += 1
These do not need a new axiom:
$$A \cap B = \{x \in A : x \in B\}$$i.e., we are using the property $p = p(x) = x \in B$ with free variable $x$.
Remark: By axiom of extenstion $A \cap B = B \cap A$.
val A = Set(1, 2, 3)
val B = Set(2,3, 7, 9)
A intersect B
A.filter(x => B contains x)
The power set of a set $S$ is the set of subsets of $S$, i.e. $$2^S = \{x : x \subset S\}$$
This exists because of the axiom of power sets (which just says it exists).
Set(1, 2, 7).subsets.toSet
Set().subsets.toSet
Set().subsets.toSet.size
Formally, we define $A \subset B$ by $x\in A \implies x \in B$.
The axiom giving existence of power sets says $$\forall S\exists P (x\in P \iff x\subset S)$$
or in full form $$\forall S\exists P (x\in P \iff (\forall y\ y\in x\iff y\in S))$$
Everything in mathematics can be represented as sets. As an example, we consider natural numbers. We associate to each number $n$ a set of size n.
In general, we define the successor of a set $s$ as $$succ(s) = s \cup \{s\}$$ and define the set associated to $n$ by
Remark: $\{s\} = \{y \in 2^s: y = s \}$
def succ(s: Set[Any]) : Set[Any] = s union Set(s)
succ(Set(1, 2))
def numberSet(n: Int): Set[Any] =
if (n == 0) Set() else succ(numberSet(n - 1))
numberSet(3)
(0 to 10).map (n => numberSet(n).size)
Talking of size is circular. Instead Cantor defined when two sets have the same size. Formally, we say same cardinality.
We say two sets have the same cardinality if there is a one-to-one correspondence between their elements.
By this definition, natural numbers and even natural numbers have the same cardinality.
A function $f: X \to Y$ is given by
Example: We can take $X = Y = \mathbb{N}$ and define $f(n) = 2n$.
A function $f: X \to Y$ is said to be injective if for $a, b\in X$, if $a\neq b$ then $f(a)\neq f(b)$, i.e. $$\forall a,b\in X, a\neq b\implies f(a)\neq f(b)$$
Equivalently, $$\forall a, b\in X, (a = b) \lor (f(a) \neq f(b))$$
def isInjective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
domain.forall{a =>
domain.forall{b =>
(a == b) || (f(a) != f(b))}}
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => 2 * n)
isInjective((1 to 10).toSet, (1 to 30).toSet, (n: Int) => n/ 2)
isInjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
isInjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))
The range of $f: X \to Y$ is defined as $$f(X) = \{f(x): x \in X\}$$
We say $f: X \to Y$ is surjective if $f(X) = Y$.
def range[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
domain.map(f)
range(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
range(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))
def isSurjective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
range(domain, codomain, f) == codomain
isSurjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 2, 3 -> 1))
isSurjective(Set(1, 2, 3), Set(1, 2, 3), Map(1 ->1, 2 -> 3, 3 -> 2))
isSurjective(Set(1, 2, 3), Set(1, 2), Map(1 ->1, 2 -> 2, 3 -> 1))
def isBijective[A, B](domain: Set[A], codomain: Set[B], f: A => B) =
isSurjective(domain, codomain, f) && isInjective(domain, codomain, f)
isBijective(Set(1, 2, 3), Set(2, 4, 6), Map(1 -> 2, 2-> 4, 3 -> 6))
isBijective(
Set(1, 2, 3), Set(1, 2, 3, 4, 5, 6), Map(1 -> 2, 2-> 4, 3 -> 6)
)
isBijective(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2-> 1, 3 -> 1))
If $f: X \to Y$ is a bijection, then it has an inverse $f^{-1}: Y\to X$ so that $$\forall x\in X, f^{-1}(f(x)) = x$$ and $$\forall y\in Y, f(f^{-1}(y)) = y$$ and conversely. Further, $f^{-1}: Y \to X$ is a bijection.
def inverseFunction[A, B](domain: Set[A], codomain: Set[B], f: A => B) ={
require(isBijective(domain, codomain, f),
"can only invert bijections")
(y: B) => domain.find(x => f(x) == y).get
}.ensuring{
g =>
domain.forall(x => g(f(x)) == x) &&
codomain.forall(y => f(g(y)) == y)
}
inverseFunction(Set(1, 2, 3), Set(1, 2, 3), Map(1 -> 2, 2 ->3, 3 -> 1))
Try{
inverseFunction(Set(1, 2, 3),
Set(1, 2, 3), Map(1 -> 2, 2 ->1, 3 -> 1))
}
def inverseMap[A, B](domain: Set[A], codomain: Set[B], f: A => B) ={
require(isBijective(domain, codomain, f),
"can only invert bijections")
(codomain.map{
(y: B) => y -> domain.find(x => f(x) == y).get}).toMap
}.ensuring{
g =>
isBijective(codomain, domain, g) &&
domain.forall(x => g(f(x)) == x) &&
codomain.forall(y => f(g(y)) == y)
}
inverseMap(Set(1, 2, 3), Set(4, 5, 6), Map(1 -> 4, 2 -> 6, 3 -> 5))
Theorem: For any set $S$, any function $f: S \to 2^S$ is not a surjection. In particular $S$ and $2^S$ do not have the same cardinality.
In other words, if $f: S\to 2^S$, there exists $y\in 2^S$ such that $y\notin f(S)$.
Proof: We define $y\in 2^S$, i.e., $y\subset S$, which is not in the range by $$y = \{x \in S: x \notin f(x)\}$$
This is not in $f(S)$ as for all $x_0\in X$, then observe that $$x_0\in y \iff x_0 \notin f(x_0)$$ so $y\neq f(x_0)$.
def cantor[A](s: Set[A], f: A => Set[A]): Set[A] =
s.filter{x => !f(x).contains(x)
}.ensuring(t => !range(s, s.subsets.toSet, f).contains(t))
cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2, 3)))
cantor(Set(1, 2, 3), Map(1 -> Set(1), 2 -> Set(1, 2), 3 -> Set(1, 2)))
This is a hotel with infinitely many rooms, with number $1$, $2$, $3$, $4$, ...
We have defined what it means for sets $A$ and $B$ to have the same size. We denote this $|A| = |B|$ (for now $|A|$ has no meaning).
Question: When should we say $|A| \leq |B|$?
Definition: We say $|A| \leq |B|$ if there is an injective function from $f: A \to B$.
Question: If $|A| \leq |B|$ and $|B| \leq |A|$, does it follow that $|A| = |B|$?
Answer: Yes. This is the Cantor-Bernstein-Shroeder theorem.
Question (Trichotomy): Given sets $A$ and $B$, is at least one of $|A| \leq |B|$ and $|B| \leq |A|$ true?
Answer: Yes. Follows from the following.
Proposition: There are subsets $C \subset A$ and $D \subset B$ and a bijection from $C$ to $D$ such that either $C = A$ or $D = B$.
That is, there is either a bijection from a subset of $A$ to all of $B$ or from $A$ to a subset of $B$.
def trichotomy[X, Y](A : Set[X], B: Set[Y]) : Map[X, Y] = {
if (A.isEmpty || B.isEmpty) Map[X,Y]()
else {
val x = A.head
val y = B.head
trichotomy[X, Y](A - x, B - y) + (x -> y)
}
}.ensuring{(f : Map[X, Y]) => (f.keySet == A || f.values.toSet == B) &&
f.keySet.subsetOf(A) &&
f.values.toSet.subsetOf(B) &&
isBijective(f.keySet, f.values.toSet, f)
}
trichotomy(Set(1, 2, 4), Set(1, 4, 5, 7))
trichotomy(Set(true, false), Set(3, 4, 5))
trichotomy(Set(1, 2, 4), Set("Hello", "Hi"))
In the finite case, this terminates by induction. In general, we have to use transfinite induction.
Definition: A set $A$ is said to be countable if $|A| \leq |\mathbb{N}|$. Otherwise we say it is uncountable.
Propn: If $A$ is countable either $A$ is finite or $|A| = \mathbb{N}$
A relation $R$ on a set $A$ is a subset of $A \times A$. We think of $(a, b)\in R$ as $A$ is related to $R$.
Examples:
def relation[A](s: Set[A], property : (A, A) => Boolean) =
for {
x <- s
y <- s
if property(x, y)
} yield (x, y)
val s = (1 to 10).toSet
val diffDiv3 = relation[Int](s, {(x, y) => (x - y) % 3 == 0})
val divides = relation[Int](s, (x, y) => y % x == 0)
val sumDiv3 = relation[Int](s, (x, y) => (x + y) % 5 == 0)
def isReflexive[A](s: Set[A], r: Set[(A, A)]) =
s.forall(x => r.contains((x, x)))
isReflexive(s, diffDiv3)
isReflexive(s, divides)
isReflexive(s, sumDiv3)
def isSymmetric[A](s: Set[A], r: Set[(A, A)]) =
r == r.map{case (x, y) => (y, x)}
isSymmetric(s, diffDiv3)
isSymmetric(s, divides)
isSymmetric(s, sumDiv3)
def isTransitive[A](s: Set[A], r: Set[(A, A)]) : Boolean =
s.forall{a =>
s.forall{b =>
s.forall{c =>
!r.contains((a, b)) || !r.contains((b, c)) ||
r.contains((a, c)) }}}
isTransitive(s, divides)
isTransitive(s, diffDiv3)
isTransitive(s, sumDiv3)
If a relation $R$ does not have one or more of these properties, we find the smallest relation on $S$ that contains $R$ and has the property.
def reflexiveClosure[A](s: Set[A], r: Set[(A, A)]) =
{r union s.map{a => (a, a)}}.ensuring{r1 => isReflexive(s, r1) && r.subsetOf(r1)}
reflexiveClosure(s, sumDiv3)
def symmetricClosure[A](s: Set[A], r: Set[(A, A)]) =
{r union r.map{case (a, b) => (b, a)}}.ensuring{
r1 => isSymmetric(s, r1) && r.subsetOf(r1)
}
symmetricClosure(s, divides)
val diff2 = relation[Int](s, (x, y) => y -x == 2)
isTransitive(s, diff2)
def transiviteClosureStep[A](s: Set[A], r: Set[(A, A)]) =
r union {
for {
a <- s
b <- s
c <- s
if r.contains((a, b)) && r.contains((b, c))
} yield (a, c)
}
transiviteClosureStep(s, diff2)
def transitiveClosure[A](s: Set[A], r : Set[(A, A)]) : Set[(A, A)] = {
val nextStep = transiviteClosureStep(s, r)
if (r == nextStep) r else transitiveClosure(s, nextStep)
}.ensuring{r1 => isTransitive(s, r1) && r.subsetOf(r1) }
transitiveClosure(s, diff2)
An equivalence relation is a relation that is reflexive, symmetric and transitive.
def isEquivalence[A](s: Set[A], r: Set[(A, A)]) : Boolean =
isReflexive(s, r) && isSymmetric(s, r) && isTransitive(s, r)
def equivalenceClosure[A](s: Set[A], r: Set[(A, A)]) =
transitiveClosure(s, symmetricClosure(s, reflexiveClosure(s, r))).
ensuring{
r1 => isEquivalence(s, r1) && r.subsetOf(r1)
}
val equivDiff2 = equivalenceClosure(s, diff2)
We say the orbit of $x$ in an equivalence relation $R$ is $$\{y \in S: (x, y)\in R\}$$
def orbit[A](x: A, s: Set[A], r: Set[(A, A)]) =
s.filter{y => r.contains((x, y))}
def orbitMap[A](s: Set[A], r: Set[(A, A)]) =
s.map{x => x -> orbit(x, s, r)}
orbitMap(s, equivDiff2)
orbitMap(s, diffDiv3)
Thus, for an equivalence relation $R$ on $S$, the orbits form a partition of $S$, i.e., we get a collection of disjoint sets whose union is $S$. These are called equivalence classes.
Furthermore, two elements $x$ and $y$ are related if and only if they both belong to some equivalence class.
orbitMap(s, sumDiv3)
isEquivalence(s, sumDiv3)
orbitMap(s, diff2)
orbitMap(Set(1, 2, 3, 4), Set((1, 1),(1, 3), (2, 2), (2, 3), (3, 1)))
A type theory means:
In scala and most other languages, we have various types we can form. The most important is that given types $A$ and $B$, we can form the function type $A \to B$.
val next : Int => Int = (n: Int) => n + 1
There are also prebuilt types and type constructors: pairs, unit and zero (nothing)
(3, 4)
(3, "Hello World")
() : Unit
The Unit type is a type with just one object (in scala it is also called Unit).
println _
val result = println("Hello types")
result
Unit
We also have inductive types, which are types whose objects are generated by given introduction rules. In scala these are given by a sealed trait
and case class
(or case object
) statements.
sealed trait BinTree
case object Leaf extends BinTree
case class Node(left: BinTree, right: BinTree) extends BinTree
val egTree : BinTree = Node(Node(Leaf, Leaf), Node(Node(Leaf, Leaf), Leaf))
Functions on these can be defined by recursion/induction.
def vertices(t: BinTree) : Int = t match {
case Leaf => 1
case Node(t1, t2) => vertices(t1) + vertices(t2) + 1
}
vertices(egTree)
Types, including inductive types, can depend on other types. For example, we can define Labelled trees labelled with leaves having labels in $A$. We call these type families.
sealed trait LabelledTree[A]
case class LabelledLeaf[A](label: A) extends LabelledTree[A]
case class LabelledNode[A](
left: LabelledTree[A], right: LabelledTree[A]
) extends LabelledTree[A]
val egLT = LabelledNode(LabelledLeaf(1),
LabelledNode(LabelledLeaf(2), LabelledLeaf(3)))
val stringyTree = LabelledNode(LabelledLeaf("Hello"),
LabelledNode(LabelledLeaf("Tree"),
LabelledLeaf("with labels")))
def labels[A](t: LabelledTree[A]) : Vector[A] = t match {
case LabelledLeaf(l : A) => Vector(l)
case LabelledNode(t1, t2) => labels(t1) ++ labels(t2)
}
labels(egLT)
labels(stringyTree)
def cannotDefine : Nothing = ??? // Nothing is a type with no objects
A type system at this level allows us to check some properties, but not all at the level of syntax (i.e. at compile time).
// math.sqrt("Hello world") - will not compile
Try(math.sqrt(-1)) // this will compile
For example, if we want to take half of only even integers, we can do this using require and ensuring but not at type level (in a simple way).
def half(n: Int) : Int = {
require(n %2 == 0, "cannot take half of an odd number")
n /2
}
def double(n: Int) : Int = (2 * n).ensuring{k => k % 2 == 0}
def halfDouble(n: Int) = half(double(n))
(1 to 10).map(halfDouble)
Try(half(3))
In dependent type theory, we will have types that represent, for example, that a number is even. Specifically
// A bad definition
def recHalf(n: Int) : Int = if (n == 0) 0 else recHalf(n - 2) + 1
recHalf(10)