+ 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;
  println$ \(\Gamma\)\(\alpha\);

+ 1.2 Ceil and Floor

Pair \lceil,\rceil and \lfloor,\rfloor, mapped by the parser to the functions ceil and floor, defined for real floating types. The result is a floating type, not an integer!

  println$ \(\lceil x + 2.3 \rceil + \lfloor 2.3 \rfloor + 0.1\);

+ 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 \);
  println$ \( \lVert 1,2,3 \rVert \);

+ 1.4 Sqrt

The square root is only available in math mode. Unless it's argument is a single symbol, grouping operators are required to get the overline in the right place.

  var x = 4.0;
  println$ \( \sqrt {(x + 2.0 )}\);

+ 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.

  println$ \(x + 1.0 \over 2.0\);

+ 1.6 Bracket forms

The two bracket forms \brace and \brack have the same precedence as \over and map to arbitrary binary functions of two arguments. They require mathmode to display correctly.

  fun \(\brace\) (x:int, y:int) => x + 2 * y;
  fun \(\brack\) (x:int, y:int) => x + 2 * y;
  println$ \( 2 \brace 3 \) + \( 2 \brack 3 \);

+ 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$ "abaa" \(\in\) RE2 "(a|b)*a";

+ 2.2 Set forms

Felix provides a construction known as a set form which defines a set like object based on a predicate. The syntax is { pattern : type | boolexpr } where you can also use \{\} brackets and \| or \mid for the vertical bar.

Technically a set form is a value of type set_form[T] which is an object with a method has_elt : T -> bool. We then provide the membership operator for set forms so you can write code like this:

  var oddints = { x : int | x % 2 == 1 };
  println$ 1 \(\in\) oddints;
  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;
  println$ 2 \(\wedge\) 3, 2 \(\vee\) 3;

+ 4 Boolean

There are some fancy logic operators.

  println$ \(\lnot\) (true \(\land\) true \(\lor\) false \(\implies\) false);

+ 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
    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;