API

Prop

The set of propositions, which are statements that are either true or false.

∧(props...)
p ∧ q

Conjunction of two or more propositions.

R

The field of real numbers.

Rⁿ

A real finite-dimensional vector space of arbitrarily large dimension. Note that the superscript n does not refer to the variable n, but is simply part of the symbol for the vector space (Rⁿ is a single symbol in Julia). To create other similar vector spaces, just create an abstract type that subtypes VectorSpace{R}, such as:

abstract type Rᵐ <: VectorSpace{R} end

Sⁿ

A real finite-dimensional vector space of symmetric matrices.

0 ⪯ A

Proposition that a symmetric matrix is positive semidefinite.

A ⪰ 0

Proposition that a symmetric matrix is positive semidefinite.

tr(A)

Trace of a symbolic matrix.

⋅(x,y)
x ⋅ y

Inner product of two vectors.

• For scalars, this is standard multiplication.
• For vectors, this is x'(y).
• For matrices, this is tr(A * B).

functional(V)

Create a symbolic functional from a vector space V to its underlying scalar field.

differentiable_functional(V)

Create a symbolic differentiable functional from a vector space V to its underlying scalar field. For a differentiable function f, access its gradient as f'.

convex(f)

Proposition that the differentiable symbolic function f is convex.

smooth_convex(f, L)

Proposition that the differentiable symbolic function f is L-smooth and convex.

smooth_strongly_convex(f, μ, L)

Proposition that the differentiable symbolic function f is L-smooth and μ-strongly convex.

sector_bounded(f, μ, L)

Proposition that the differentiable symbolic function $f$ is $[\mu,L]$ sector bounded, meaning that

\[ ( \nabla f(x) - \mu x )^\top ( \nabla f(x) - L x ) \leq 0\]

for all vectors $x$ in the domain of $f$.

@alg ex

Domain-specific language (DSL) for algorithmic computation. Constructs symbolic variables and assigns symbolic expressions.

Syntax Rules

1. Variables (∈ or in)

   Declare symbolic variables belonging to a specific space:

   • Single variable: x ∈ R or x in R
   • Tuple syntax: x, y ∈ R
   • Multiple types on single line: x ∈ Rⁿ, y ∈ Rᵐ

2. Assignments (=)

   Assign a symbolic expression to a variable:

   • z = 2x - 3y

All expressions are labeled with the symbol used to represent the quantity in the code. Also, all code constructed by the macro returns nothing to suppress verbose output. The macro is often used with begin..end or let...end blocks to specify multiple lines of statements that are evaluated sequentially.

Example

@alg let
    # Variables
    a ∈ R, u ∈ Rⁿ

    # Assignment
    z = a * u
end

simplify(expr)

Simplify an expression using any of the available transformations.

leaves(node)

Recursively collects all AST leaf nodes (nodes where iscall(v) is false) from an expression tree. Returns a Set of unique leaf nodes.

→(x,y)
x → y

Construct a transition from node x to node y. This indicates that node x is a state of the algorithm whose value at the next iteration is y.

evaluate(expr)

Evaluate an expression. Uses the following evaluation techniques (in order):

• If the expression is a parameter, return its parameter value.
• If the expression is in an active JuMP model, then its value in the model (either numeric if the model is solved, or as a JuMP expression) is returned.
• If the expression is a leaf and has an instantation as a JuMP variable, then instantiate it in the model.
• If the expression is a top-level node (e.g., a Lyapunov certificate or bisection), then evaluate the expression from the top down.
• If the expression is a basic arithmetic operation (e.g., +, -, *, /), evaluate the expression from the bottom up (starting with leaf nodes).
• If the expression has an instantation as a JuMP variable (and is not a leaf), then instantiate it in the model.

Otherwise, when none of these evaluation techniques are applicable, the original expression is returned.

with_numerics(code;
    T = Float64,
    model_constructor = () -> default_model(T),
    parameters = Dict())

Execute code within a local scope with the given JuMP model with data type T and (additional) parameters.

with_parameters(code, parameters::Dict)

Execute code within a local scope in which the parameters have the given values. This is typically called with the following syntax:

with_parameters(parameters) do
    code
end

with_additional_parameters(code, parameters::Dict)

Execute code within a local scope in which the parameters have the given values. This adds the parameters to those already in scope.

with_parameters(some_parameters) do
    some_code
    with_additional_parameters(more_parameters) do
        more_code
    end
end

minimize(obj, con)

Minimize an objective subject to a constraint.

maximize(obj, con)

Maximize an objective subject to a constraint.

feasible(con)

Determine whether or not a constraint is feasible.

Examples

@alg let
    x ∈ R
    A = [-2 x; x -2]
    with_numerics() do
        evaluate(feasible(A ⪰ 0))
    end
end

objective(opt)

Objective function of an optimization problem, which is a symbolic node in R.

constraint(opt)

Constraint of an optimization problem, which is a symbolic node in Prop.

certify(constraint, performance, rate)

Construct a Lyapunov certification problem. This searches for a parameterized Lyapunov function which certifies that the performance measure subject to the constraint converges with the specified rate.

To search for a Lyapunov certificate, the algorithm must have a state as specified by transitions within the constaint. For a state x and next state x₊, a valid Lyapunov certificate V(x) must satisfy the following conditions:

1. V(x) ≥ performance(x)
2. V(x⁺) ≤ rate * V(x)

Together, these imply that performance decreases by a factor of rate at each iteration of the algorithm. To make the search tractable, the Lyapunov candidate is parameterized linearly in the state so that V(x) = θ ⋅ x with parameter vector θ. This node evaluates to a proposition that specifies whether or not such a Lyapunov certificate exists.

rate(constraint, performance)

Construct a Lyapunov certification problem that finds the fastest rate for which a Lyapunov certificate exists. This node evaluates to the minimal rate for which certify holds.

convex_interpolation(opt::Node)

Given an optimization node, replaces all convex functions with their interpolation conditions.

smooth_convex_interpolation(opt)

Given an optimization node, replaces all smooth convex functions with their interpolation conditions.

smooth_strongly_convex_interpolation(opt)

Given an optimization node, replaces all smooth convex functions with their interpolation conditions.

sector_bounded_interpolation(opt::Node)

Given an optimization node, replaces all sector functions with their interpolation conditions.

gram_transformation(opt)

Given an optimization node, for each vector space, replaces all vectors in the space with the condition that their Gram matrix is positive semidefinite. All inner products are flattened into new symbolic variables.

lyapunov_transformation(node)

Given a Lyapunov certificate node, constructs an optimization problem that searches for a valid Lyapunov certificate of convergence. The Lyapunov candidate is linear in the algorithm state, where the state is specified by transitions: $V(x) = \theta ⋅ x$. The analysis then uses the S-procedure to search for the parameters $\theta$ such that the Lyapunov candidate satisfies the following two conditions:

• Positivity: $V(x) \geq \text{performance}$
• Decreasing: $V(x₊) \leq \text{rate}\,V(x)$

where the performance measure and rate are specified by the node.

with_verbose(code, verbose = true)

Creates a local scope with a given verbosity.

Example

with_verbose() do
    code
end