Control

Finite-horizon control experiments. All simulation logic is ordinary Aeon; Math supplies only the existing scalar numeric primitives.
Imports
import Math;
Table of Contents

Types

Control

(inductive)
inductive Control

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Control (inductive)

result

constructor
Control

Functions

loss

def loss (episode : Control) : Float

steps

def steps (episode : Control) : Int

failed

def failed (episode : Control) : Bool

square

def square (x : Float) : Float

clip

def clip (x : Float) (lo : Float) (hi : Float | hi ≥ lo) : {v : Float | lo ≤ v && v ≤ hi}

angle

[-pi, pi); flooring handles negative angles and multiple revolutions.
def angle (theta : Float) : Float

simulate

Check failure before the fuel test, including the state reached by the last permitted transition. Failures incur a large loss, never a cheap short run.
def simulate (fuel : Int) (elapsed : Int) (total : Float) (advance : (s : a) → a) (cost : (s : a) → Float) (invalid : (s : a) → Bool) (state : a) : Control

rollout

def rollout (horizon : Int | horizon ≥ 0 && horizon ≤ 500) (advance : (s : a) → a) (cost : (s : a) → Float) (invalid : (s : a) → Bool) (initial : a) : Control