-
Notifications
You must be signed in to change notification settings - Fork 0
Standard library
These are useful definitions of sets and functions that are collected into a standard library file.
| Nat = {n∈Int | n>=0}
| PosInt = {n∈Int | n>0}
| NegInt = {n∈Int | n<0}
SetOf is a function that is applied to a set and returns a set. E.g.:
-
SetOf Numis the set of sets of numbers -
SetOf (SetOf Int)is the set of sets of sets of integers
Some equivalent definitions of SetOf:
| SetOf =
{S∈Set -> {⊂ S}}
| SetOf = Set=>Set ∩
{S -> {⊂ S}}
Normally a domain failure in an inner context is not propagated to an outer context, but this definition of SetOf propagates to the outer context a domain failure of the ⊂ operation in the inner context, via inequality with the empty set:
| SetOf =
{S -> {⊂ S} ≠ {}}
SeqOf is a function that is applied to a set and returns a set. E.g., SeqOf Int is the set of sequences with integer values.
Some equivalent definitions of SeqOf:
| SeqOf = {S∈Set -> {s ∈ Seq | Im s ⊂ S}}
| SeqOf = {S∈Set -> {∈ Seq ∩ Int=>S}}
Normally a domain failure in an inner context is not propagated to an outer context, but this definition of SeqOf propagates to the outer context a domain failure of the => operation in the inner context, via inequality with the empty set:
| SeqOf = {S -> {∈ Seq ∩ Int=>S} ≠ {}}
Boolean operations apply only to booleans, otherwise have no values.
∧ and ∨ are the conjunction and disjunction operators.
∧ and ∨ can also be written as && and ||.
#opl 6 ∧ &&
#opl 5 ∨ ||
| (∧) = (&&) =
{true -> true -> true,
true -> false -> false,
false -> true -> false,
false -> false -> false,
false -> null -> false,
null -> false -> false,
}
| (∨) = (||) =
{true -> true -> true,
true -> false -> true,
false -> true -> true,
false -> false -> false,
true -> null -> true,
null -> true -> true,
}
This definition of ∨ allows x ⊂ T ∨ x = 0, when x = 0, to be true rather than have no values.
--> is the implication operator.
--> can also be written as ⟶.
#opr 4 --> ⟶
| (-->) = (⟶) =
{true -> true -> true,
true -> false -> false,
false -> true -> true,
false -> false -> true,
false -> null -> true,
null -> true -> true,
}
These definitions of ∧, ∨ and --> are consistent with each other by De Morgan's laws.
? is the first operator in a ternary conditional. The second operator in a ternary conditional is $, the application operator. ? has higher precedence than $, so a ternary conditional expression doesn't need parentheses within it.
cond ? then $ else has the values of then if cond is true (even when else has no values), and the values of else if cond is false (even when then has no values).
? is non-associative.
#op 3 ?
| (?) =
{true -> then -> else -> then,
true -> then -> null -> then,
false -> then -> else -> else,
false -> null -> else -> else,
}
The restriction operator => produces a set useful for restricting, by intersection, the domain and image of a function.
=> can also be written as ⇒.
=> is a cross product for arrows. A=>B=>C is equivalent to {∈A->∈B->∈C}.
One way to express the image of a set S under a function f is Im(f ∩ S=>Any).
#opl 13 => ⇒
| (=>) = (⇒) =
{S∈Set -> T∈Set -> {∈S -> ∈T}}
\ is set difference, a.k.a. relative complement of sets.
#opl 14 \
| (\) = Set=>Set=>Set ∩
{A -> B -> {x∈A | x∉B}}
f ∘ g is the composition of generalized functions f and g. Thus (f ∘ g) x is equivalent to f (g x).
∘ can also be written as ..
#opr 19 ∘ .
| (∘) = (.) = {f -> g -> x -> f (g x)}
f $ g $ x is equivalent to f (g x), where f and g are generalized functions.
#opr 2 $
| ($) = {f -> x -> f x}
The operator ;; creates a set of tags from an existing set.
#opr 16 ;;
| (;;) =
{type∈Sym -> S∈Set -> {type;s | s∈S}}
¬ applies only to booleans.
#name ¬ !
| ! = ¬ = {true -> false, false -> true}
| if = (?)
| id = {x -> x}
| const = {x -> {_ -> x}}
| inc = {x -> x+1}
| dec = {x -> x-1}
| first = {x:_ -> x}
| rest = {_:xs -> xs}
Three equivalent definitions of second:
| second = {_:x:_ -> x}
| second = {s -> first(rest s) | len s≥2}
The | len s≥2 can be omitted, because first(rest s) will return no values if the length of s is zero or one:
| second = {s->first(rest s)}
| take = Nat=>Seq=>Seq ∩
{0 -> _ -> [],
n -> x:xs -> x: take(dec n)xs
}
map applies a generalized function to each element of a sequence to form another sequence.
| map = Any=>Seq=>Seq ∩
{_ -> [] -> [],
f -> x:xs -> f x : map f xs
}
| filter = Set=>Seq=>Seq ∩
{_ -> [] -> [],
S -> x:xs -> x∈S ? x:r $ r |r=filter S xs
}
| remove = Set=>Seq=>Seq ∩
{_ -> [] -> [],
S -> x:xs -> x∈S ? r $ x:r |r=remove S xs
}
| reduce = foldl = SetOf(Any=>Any=>Any)=>Any=>Seq=>Any ∩
{_ -> z -> [] -> z,
f -> z -> x:xs -> foldl f (f z x) xs
}
| foldr = SetOf(Any=>Any=>Any)=>Any=>Seq=>Any ∩
{_ -> z -> [] -> z,
f -> z -> x:xs -> f x (foldr f z xs)
}
| mapcat = SetOf(Any=>Seq)=>Seq=>Seq ∩
{f -> s -> reduce(++) [] (map f s)}
Several definitions of zip are given, illustrating various approaches to type policy.
The first two definitions use simple type assertions that cover all cases.
| zip =
{a∈Seq -> b∈Seq
-> [] | a=[] ∨ b=[],
-> [x,y]: zip xs ys
| a=x:xs
| b=y:ys
}
| zip = Seq=>Seq=>Seq ∩
{[] -> _ -> [],
_ -> [] -> [],
x:xs -> y:ys -> [x,y]: zip xs ys
}
The next definition is an example of declaring a type only for the cases that aren't implicitly typed, where the function has an overall non-dependent type.
| zip =
{[] -> ∈Seq -> [],
∈Seq -> [] -> [],
x:xs -> y:ys -> [x,y]: zip xs ys
}
The last definition has no explicit type assertions, thereby allowing one argument to be a non-sequence when the other argument is [], which means the function has a dependent type.
| zip =
{[] -> _ -> [],
_ -> [] -> [],
x:xs -> y:ys -> [x,y]: zip xs ys
}
A simple way to coerce a set S into a function is to intersect S with Arr to remove non-arrows, but this doesn't always yield a function with the same domain and image sets as S, when S is treated as a generalized function.
toFn x, where x∈Any is treated as a generalized function, yields a function with the same domain and image sets as x.
toArr coerces an object to multivalued arrows. toFn coerces an object to a function by wrapping the arrows generated by toArr in a set.
| toFn =
{x -> toArr x}
| toArr =
{a∈Arr -> a,
_;x -> toArr x,
S∈Set -> toArr x |x ∈ S
}
| tagType = {t;_ -> t}
| tagValue = {_;v -> v}