Grammar

Below is the approximate BNF grammar for Kotlin∇. This is incomplete and subject to change without notice.

#Numerical types:

1  𝔹 = "True" | "False"
2  𝔻 = "1" | ...  | "9"
3  ℕ =  𝔻  | 𝔻"0" | 𝔻ℕ
4  ℤ = "0" | ℕ    | -ℕ
5  ℚ = ℕ | ℤ"/"ℕ
6  ℝ = ℕ | ℕ"."ℕ | "-"ℝ
7  ℂ = ℝ + ℝi
8  ℍ = ℝ + ℝi + ℝj + ℝk
9  T = 𝔹 | ℕ | ℤ | ℚ | ℝ | ℂ | ℍ
10  n = ℕ < 100*
11vec = [Tⁿ]
12mat = [[Tⁿ]ⁿ]

^∗ To increase n, see DimGen.kt.

#DSL

1       type = "Double" | "Float" | "Int" | "BigInteger" | "BigDouble";
2        nat = "1" | ... | "99";
3     output = "Fun<" type "Real>" | "VFun<" type "Real," nat ">" | "MFun<" type "Real," nat "," nat ">";
4        int = "0" | nat int;
5      float = int "." int;
6        num = type "(" int ")" | type "(" float ")";
7        var = "x" | "y" | "z" | "ONE" | "ZERO" | "E" | "Var()";
8     signOp = "+" | "-";
9      binOp = signOp | "*" | "/" | "pow";
10     trigOp = "sin" | "cos" | "tan" | "asin" | "acos" | "atan" | "asinh" | "acosh" | "atanh";
11    unaryOp = signOp | trigOp | "sqrt" | "log" | "ln" | "exp";
12        exp = var | num | unaryOp exp | var binOp exp | "(" exp ")";
13    expList = exp | exp "," expList;
14      linOp = signOp | "*" | " dot ";
15        vec = "Vec(" expList ")" | "Vec" nat "(" expList ")";
16     vecExp = vec | signOp vecExp | exp "*" vecExp | vec linOp vecExp | vecExp ".norm(" int ")";
17        mat = "Mat" nat "x" nat "(" expList ")";
18     matExp = mat | signOp matExp | exp linOp matExp | vecExp linOp matExp | mat linOp matExp;
19     anyExp = exp | vecExp | matExp | derivative | invocation;
20   bindings = exp " to " exp | exp " to " exp "," bindings;
21 invocation = anyExp "(" bindings ")";
22 derivative = "d(" anyExp ") / d(" exp ")" | anyExp ".d(" exp ")" | anyExp ".d(" expList ")";
23   gradient = exp ".grad()";

Operational Semantics

Below we provide an operational semantics for Kotlin∇.

1                 v = a | ... | z | vv
2                 c = 1 | ... | 9 | cc | c.c
3                 e = v | c | e ⊕ e | e ⊙ e | (e) | (e).d(v) | e(e = e)
4                 
5       d(e) / d(v) = e.d(v)
6      Plus(e₁, e₂) = e₁ ⊕ e₂
7     Times(e₁, e₂) = e₁ ⊙ e₂
8           c₁ ⊕ c₂ = c₁ + c₂
9           c₁ ⊙ c₂ = c₁ * c₂
10       e₁(e₂ = e₃) = e₁[e₂ → e₃]
11           
12    (e₁ ⊕ e₂).d(v) =    e₁.d(v)   ⊕   e₂.d(v)
13    (e₁ ⊙ e₂).d(v) = e₁.d(v) ⊙ e₂ ⊕ e₁ ⊙ e₂.d(v)
14          v₁.d(v₁) = 1
15          v₁.d(v₂) = 0
16            c.d(v) = 0
17
18     e.d(v₁).d(v₂) = e.d(v₂).d(v₁) †
19
20(e₁ ⊕ e₂)[e₃ → e₄] = e₁[e₃ → e₄] ⊕ e₂[e₃ → e₄]
21(e₁ ⊙ e₂)[e₃ → e₄] = e₁[e₃ → e₄] ⊙ e₂[e₃ → e₄]
22       e₁[e₁ → e₂] = e₂
23       e₁[e₂ → e₃] = e₁

In the notation above, we use subscripts to denote conditional inequality. If we have two nonterminals with matching subscripts in the same production, i.e. eₘ, eₙ where m = n, then eₘ = eₙ must be true. If we have two nonterminals with different subscripts in the same production, i.e. eₘ, eₙ where m ≠ n, either eₘ = eₙ or eₘ ≠ eₙ may be true. Subscripts have no meaning across multiple productions.

^† See Clairaut-Schwarz. Commutativity holds for twice-differentiable functions, however it is possible to have a continuously differentiable function whose partials are defined everywhere, but whose permuted partials are unequal ∂F²/∂x∂y ≠ ∂F²/∂y∂x. Some examples of continuously differentiable functions whose partials do not commute may be found in Tolstov (1949, 1949).

Reduction semantics

Our reduction semantics can be described as follows:

Sub loosely corresponds to η-reduction in the untyped λ-calculus, however f ∉ Ω is disallowed, and we assume all variables are bound by Inv. Let us consider what happens under f∶ {a, b, c} ↦ abc, g∶ {a, b, c} ↦ ac under Ω ∶= {(a, 1), (b, 2), (c, 2)}:

We can view the above process as acting on a dataflow graph, where Inv backpropagates Ω, and Sub returns concrete values Y, here depicted on g: