Prev

f arg := exp <=> f := exp @ arg

fac (n>1) := n*fac(n-1)

application is so useful there are multiple ways (at different orders and operator precedence) to express it

f x <=> f`x <=> f <| x <=> x |> f <=> (`x) f

(f$g) <| x := f <| g <| x

FNil <| x := x

[f] either applies f or returns the argument unchanged. {f} applies f until reaching a fixpoint.

[f] x := (f :: FNil) x

{f} x := (f && FNil) $ Star f <| x

(f&&g), (f||g), (f::g), and (f//g) are analogous to the finite map case. All except for (::) are also available at (*),(%), and (/) respectively.

patterns

A constant in patterns is checked for equality. (_) in a pattern is a don't care.

Variables in patterns are bound.

Unary ops should be either constructors [qv (::=) later] or predicates.

Binary ops are handled a bit more subtly: relational ops always bind their first argument, and only bind the second if it is not bound as a first argument elsewhere in the pattern.

So x,(y>x) binds x and y, and checks that y>x, but x,y and xs/ys bind both arguments.

(There is a special case here: (,) binds items by arity, eg x,y,z only matches sequences with exactly 3 items)

fac := (n*fac(n-1) @ (n>1) !! 1 @ (n<=1))

Const x := x @ _

fac := (n*fac(n-1) @ (n>1) :: Const(1)) NB. using nesting

eqns

unlike for finite maps, (≅) and (≲) are not computable; best we can do atm are (==) and (<=)

f ≅ g <=> f x == g x		
f ≲ g <=> f x ~ g x
f == g ==> f ≅ g
f <= g ==> f ≲ g

f ≲ g ==> (f||h) ≲ (g||h)
f ≲ g ==> (f&&h) ≲ (g&&h)
f ≲ g ==> (f!!h) ≲ (g!!h) 
f ≲ g ==> dom f~dom g ==> (f::h) ≲ (g::h)
f ≲ g ==> (h//f) ≲ (h//g)
f ≲ g ==> dom f~dom g ==> (f//h) ≲ (g//h)
f ≲ g ==> f$h ≲ g$h
f ≲ g ==> h$f ≲ h$g
f ≲ g ==> dom f~dom g ==> [f] ≲ [g]

(f||g) $ h == (f$h) || (g$h)
f $ (g||h) == (f$g) || (f$h)
(f&&g) $ h == (f$h) && (g$h)
f $ (g&&h) == ((f$G g)||(f$G h)   $$ G: gang(g,h))
(f::g) $ h == ((F f$h)||(F g$h)   $$ F: fatbar(f,g))
f $ (g :: h) == (f$g :: f$h)

f~Total <=> not(f x~Null)
f~Total && g~Total ==> (f||g)~Total
f~Total && g~Total && (dom f & dom g)~Null ==> (f&&g)~Total
f~Total && g~Total && (dom f & dom g)~Null ==> (f!!g)~Total
f~Total && g~Total ==> (f::g)~Total
f~Total && g~Total ==> (f//g)~Total
f~Total && g~Total ==> (g//f)~Total

furthermore, if f is an element (f x is either Null, Nuts, or an element) and g is an element, the following are also elements: (f&&g), (f!!g), (f::g), (f//g), (g//f).

currying

add0 n m := n+m <=> add0 := n+m @ m @ n

add1 (n,m) := n+m <=> add1 := n+m @ n,m

add0 x y == add1(x,y)

example

gcd: min $ {x,y-x @ x,(y>x) :: x-y,y @ x,(y<x)}

Next