# 1 Boolean Logic

`share/lib/std/scalar/bool.flx`

```  typedef bool = 2;

Standard operations on boolean type.
open class Bool
{
Short cut and via closure
noinline fun andthen (x: bool, y:1->bool) : bool =>
if x then #y else false
;

Disjunction: logical and.
fun land: bool * bool -> bool = "\$1&&\$2";      // x and y

Negated and.
fun nand: bool * bool -> bool = "!(\$1&&\$2)";   // not (x and y)

Conjunction: logical or.
fun lor: bool * bool -> bool = "\$1||\$2";       // x or y

Negated or.
fun nor: bool * bool -> bool = "!(\$1||\$2)";    // not (x or y)

Logical exclusive or.
fun xor: bool * bool -> bool = "\$1!=\$2";       // (x or y) and not (x and y)

Logical negation.
fun lnot: bool -> bool = "!\$1";                // not x

Logical implication.
fun implies: bool * bool -> bool = "!\$1||\$2";  // not x or y

Mutating or.
proc |= : &bool * bool = "*\$1|=\$2;";

Mutating and.
proc &= : &bool * bool = "*\$1&=\$2;";

// Elide double negations.
reduce dneg(x:bool): lnot (lnot x) => x;

// Elide double negations.
reduce dneg(x:bool,y:bool): lnot (nand(x,y)) => land(x,y);

// Elide double negations.
reduce dneg(x:bool,y:bool): lnot (nor(x,y)) => lor(x,y);
}

fun zero () => 0 :>> 2;
fun - (x:2) => (sub (2, caseno x)) :>> 2;
fun + (x:2, y:2) : 2 => (add ((caseno x , caseno y)) % 2) :>> 2;
fun - (x:2, y:2) : 2 => (add (2, sub(caseno x , caseno y)) % 2) :>> 2;
}

instance Str[bool] {
Convert bool to string.
fun str (b:bool) : string => if b then "true" else "false" endif;
}

instance Tord[bool] {
Total ordering of bools, false < true.
Note that x < y is equivalent to x implies y.
fun < : bool * bool -> bool = "\$1<\$2";
}

open Tord[bool];
open Show[bool];

```

# 2 Syntax

`share/lib/std/scalar/boolexpr.fsyn`

```syntax boolexpr
{
//\$ Boolean false.
satom := "false" =># "'(ast_typed_case  0 2)";

//\$ Boolean true.
satom := "true" =># "'(ast_typed_case  1 2)";

//\$ Logical implication.
x[simplies_condition_pri] := x[>simplies_condition_pri] "implies" x[>simplies_condition_pri] =># "(Infix)";

//\$ Logical disjunction (or).
x[sor_condition_pri] := x[>sor_condition_pri] ( "or" x[>sor_condition_pri])+ =># "(chain 'ast_orlist _1 _2)" note "lor";

//\$ Logical conjunction (and).
x[sand_condition_pri] := x[>sand_condition_pri] ( "and" x[>sand_condition_pri])+ =># "(chain 'ast_andlist _1 _2)" note "land";

//\$ Logical negation (not).
x[snot_condition_pri] := "not" x[snot_condition_pri]  =># "`(ast_not ,_sr ,_2)";

x[scomparison_pri]:= x[>scomparison_pri] "\not" cmp x[>scomparison_pri] =># "`(ast_not ,_sr (ast_apply ,_sr (,_3 (,_1 ,_4))))";

// tex logic operators
x[stex_implies_condition_pri] := x[>stex_implies_condition_pri]  "\implies" x[>stex_implies_condition_pri] =># "(infix 'implies)";
x[stex_or_condition_pri] := x[>stex_or_condition_pri] ( "\lor" x[>stex_or_condition_pri])+ =># "(chain 'ast_orlist _1 _2)" note "lor";
x[stex_and_condition_pri] := x[>stex_and_condition_pri] ( "\land" x[>stex_and_condition_pri])+ =># "(chain 'ast_andlist _1 _2)" note "land";
x[stex_not_condition_pri] := "\lnot" x[stex_not_condition_pri]  =># "`(ast_not ,_sr ,_2)";

bin := "\iff" =># '(nos _1)'; // NOT IMPLEMENTED FIXME
bin := "\impliedby" =># '(nos _1)'; // NOT IMPLEMENTED FIXME

//\$ Conditional expression.
satom := sconditional "endif" =># "_1";

//\$ Conditional expression (prefix).
sconditional := "if" sexpr "then" sexpr selse_part =>#
"`(ast_cond ,_sr (,_2 ,_4 ,_5))";

selif := "elif" sexpr "then" sexpr =># "`(,_2 ,_4)";

selifs := selif =># "`(,_1)";
selifs := selifs selif =># "(cons _2 _1)";

selse_part:= "else" sexpr =># "_2";
selse_part:= selifs "else" sexpr =>#
"""
(let ((f (lambda (result condthn)
(let ((cond (first condthn)) (thn (second condthn)))
`(ast_cond ,_sr (,cond ,thn ,result))))))
(fold_left f _3 _1))
""";
}

```

# 3 Predicate combinators.

A predicate is any function returning a boolean argument. Predicates are also relations by simply providing a tuple argument.

This is a simple class allowing predicates to be combined directly using symbolic operators to form new predicates, using logical conjunction `and`, disjunction `or`, implication `implies` and negation `not`. The parser maps these operator onto the functions `land`, `lor`, `implies`, and `lnot` respectively.

`share/lib/std/algebra/predicate.flx`

```
// Some operations on predicates.
// These also automatically apply to relations, but just taking
// the argument as a tuple.

open class Predicate[T]
{
fun land (f:T->bool,g:T->bool) =>
fun (x:T) => f x and g x
;

fun lor (f:T->bool,g:T->bool) =>
fun (x:T) => f x or g x
;

fun implies (f:T->bool,g:T->bool) =>
fun (x:T) => f x implies g x
;

fun lnot (f:T->bool) =>
fun (x:T) => not (f x)
;

}

```