# 1 Math in Felix

Felix provides a set of symbols from $$\TeX$$, $$\LaTeX$$ and AmSTeX which will display nicely with flx_web using the excellent MathJax package as written in Felix program code.

All symbols starting with slosh and followed by alphabetic letters are valid Felix identifiers as well as valid TeX.

Additionally Felix supports some special symbols recognized by both the language processor and MathJaX.

Felix also supports both inline and display math using MathJaX \( .. \) and \[ .. \] brackets, these work in *.flx files and in both text and code in *.fdoc files.

Hover over sole operators shows the Felix source code, with math mode, a click will open a new window showing mangled source. The flx_web processor adds { and } braces around Felix grouping operators in math mode, to ensure MathJaX respects Felix grouping.

In math mode, display may fail if explicit grouping is not used where TeX expects it.

Please note it is not enough in program code that the math forms used should be both correct \TeX as well as correct Felix. Just because it looks nice doesn't mean it will compile or evaluate correctly.

## 1.1 Ordinary names

Any TeX name defined as class ORD in TeX can be used in Felix as an identifier. This includes all the usual Greek letters.

  var $$\alpha$$ = 1;
fun $$\Gamma$$ (x:int)=> x * x;



## 1.3 Abs and norm

Using \lvert,\rvert pair or \left\lvert,\right\rvert, or \left|,\right| mapping to function abs, defined for integers, reals, and complex numbers. Using \lVert,\rVert pair or \left\lVert,\right\rVert mapping to function len, defined for container and array class data structures and strings.

  println$$$\lvert -2.3 \rvert$$; println$ $$\lvert "{\mathtt{\text{Hello}}}" \rvert$$;



## 1.5 Fractions with over

The parser recognises the \over binary operator with a low precedence and maps it to the division function /. Correct display requires math mode.



## 1.7 Negated Comparisons

Felix provides syntax to negate infix predicate symbols including comparison operators. Both not and \not can be used and are semantically equivalent, however the \not only displays correctly in math mode preceding an operator without a strikethrough.

  println$(1,2,3) $$\subset$$ (1,2); println$ (1,2,3) $$\nsubseteq$$ (1,2);
println$$${(1,2,3)} \not \subseteq {(1,2)}$$; println$ (1,2,3) not $$\subseteq$$ (1,2);
println$not $${(1,2,3)} \subseteq {(1,2)}$$; println$ $${(1,2,3)} \not \supset {(1,2)}$$;
println$not $$\subset$$ ((1,2,3),(1,2)); println$  2 $$\not$$< 1;



# 2 Set operations

## 2.1 Membership

Available for all class Set, which includes all Container. Defined for arrays, and most container types including list, varray, darray, bsarray. Defined for strings and regular expressions too. [TODO: ralist, sarray]


println$mem (2, (1,2,34)); println$ 2 in (1,2,3,4);
println$2 $$\in$$ (1,2,3,4); println$ (1,2,3,4) $$\ni$$ 2;
println$(1,2,3,4) $$\owns$$ 2; println$ 5 $$\notin$$ (1,2,3,4);
println$2 $$\in$$ varray (1,2,3,4); println$ 2 $$\in$$ darray (1,2,3,4);
println$2 $$\in$$ list (1,2,3,4); println$ char "2" $$\in$$ "1234";
println$$${(3,9)} \in {\{ x,y : {\mathtt{\text{int}}} * {\mathtt{\text{int}}} \mid x * x == y \}}$$;  ## 2.3 Set Relations Felix defines setlike relations for where the arguments are in both Streamable and Set. In some cases such as the subset or equal, we only require the left operand to be in Streamable and the right operand to be in Set. The default implementation of subset or equal streams all values of the LHS container and checks if that value is in the RHS argument. This implementation is inefficient, but it does allow the RHS to be infinite, for example a regular expression. These relations construe containers as sets and so ignore duplicates. We use the congruence operator to mean equal as sets. Two arrays, for example, may be equal as sets because they contain the same set of elements, even though the ordering is different and different elements may be duplicated, so that the arrays are not equal as arrays. Furthermore note that the operands may be completely different data structures and thus different types, however they must support the same value type.  println$ (varray (1,2)) $$\cong$$ (varray (1,2,3));
println$(varray (1,2)) $$\cong$$ (darray (1,2,2)); println$ ("aba","ababba") $$\subseteq$$ RE2 "(a|b)*a";

println$(1,2) $$\subset$$ (1,2,3); println$ (1,2) $$\subseteq$$ (varray (1,2,3));
println$(1,2) $$\subseteqq$$ (varray (1,2,3)); println$ (1,2) $$\subsetneq$$ (varray (1,2,3));
println$(1,2) $$\subsetneqq$$ (varray (1,2,3)); println$ (1,2,3) $$\supset$$ (1,2);
println$(1,2,3) $$\supseteq$$ (1,2); println$ (1,2,3) $$\supseteqq$$ (1,2);
println$(1,2,3) $$\supsetneq$$ (1,2); println$ (1,2,3) $$\supsetneqq$$ (1,2);

println$(1,2,3) $$\nsubseteq$$ (1,2); println$ (1,2,3) $$\nsubseteqq$$ (1,2);

println$(1,2) $$\nsupseteq$$ (1,2,3); println$ (1,2) $$\nsupseteqq$$ (1,2,3);



## 2.4 Set Operators

Felix currently provides set operators. They can be used with sets of type in the type language as well as with set forms. Set operators can also be used with data structures of kind Set[C,V], however the result is a set form, not a similar data structure. For example the union of two arrays is a set form that tests if an element is a member of one array or the other, not an array.

  typedef sregints = typesetof (int, long);
typedef uregints = typesetof (uint, ulong);
typedef regints = sregints $$\cup$$ uregints;
fun f[T:regints] : T -> T = "$1+1"; println$ f 1, f 1u, f 1uL;
println$10 $$\in$$ { x : int | 2 <= x } $$\cap$$ { x : int | x < 20 }; println$  10 $$\in$$ (1,2,3) $$\cup$$ (9,10,11);



# 3 Total Order

Members of class Tord provide fancy operators. Note that max uses \vee and min uses \wedge and these look the same as boolean \lor and \land but they're not. The nmemonic is to recall that both set intersection and logical conjunction make for less cases and hence \wedge is used for the minimum. Set union and logical disjunction are fatter and more inclusive and so used for the maximum.

  println$1 $$\le$$ 2; println$ 2 $$\nleq$$ 1;
println$2 $$\gt$$ 1; println$ 2 $$\geqslant$$ 1;



# 5 Quantifiers

Using the \prod and \sum symbols.

## 5.1 Sums and products of data

Sums and products of values of data structures.


println$$$\sum {(1,2,3,4)}$$ ; println$ $$\prod$$ (1,2,3,4);

println$$$\sum$$ (1,2,3,4).darray; println$ $$\prod$$ (1,2,3,4).darray;

println$$$\sum$$ (1,2,3,4).list; println$ $$\prod$$ (1,2,3,4).list;

gen odds (x:int, y:int) () = {
for var i:int in x upto y do
if y % 2 == 1 do yield Some i; done
done
return None[int];
}

println$$$\sum$$ (odds (1,7));  ## 5.2 Sums and products of functions Forms the categorical (parallel) product or sum of a tuple of functions.  fun f (x:int) : int => x + 1; fun g (x:int): string => x.str+"!"; fun h (x:double) :string => x.str+"!"; var fgx = $$\prod$$ (f,g,h); println$ fgx (1,2,3.1);

var fgs = $$\sum$$ (f,g,h);
var d1 = (case 1 of (int + int + double)) 42;
var c1 : int + string + string = fgs d1;
match c1 with
| case 0 i => println$"Case 0 " + i.str; | case 1 s => println$ "Case 1 " + s;
| case 2 s => println\$ "Case 2 " + s;
endmatch;