# Language of Epic 2

## Core Design Goals

- Excellent termination-checking properties (not Turing complete!)
- No runtime errors (extremely strong static checking)
- Minimal annotations
- Mixture of functional / procedural, I guess

Motivation: easy to write code with strong guarantees of not breaking.

### Termination Checking

[PDF about "Total Functional Programming"](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf)
[Powerpoints on decision procedures](http://www.decision-procedures.org/slides/)

All programs and subroutines will be guaranteed to terminate except for explicit sources of non-terminating behavior.

#### Beyond Primitive Recursive

The primitive recursive function are exactly those which can be computed by a programming language featuring only FOR loops. That is, the number of times any code block is executed is capped by some upper bound which is computed earlier in the code. Most functions of interest are actually primitive recursive, but the code can end up feeling extremely unnatural.

It turns out that there are ways to limit recursion so that more complex forms of always-terminating recursion are allowed. Examples include substructural recursion or Walther recursion. No matter what forms of recursion are allowed by the language, however, there will always be more complex forms of recursion that *could* be allowed but which aren't covered by the existing system. The question is to find a good match between the language syntax and the allowable recursion schemes so that common algorithms have natural implementations.

*Case Study: Ackermann's Function*

Ackermann's function is a classical example of a function that is not primitive recursive. There are, however, ways to implement Ackermann's function in languages with "primitive recursive functionals of finite type" which appears to be an extension of primitive recursion with higher-order functions.

*Case Study: GCD Euclidean Algorithm*

Example of a halting algorithm where the proof of termination is nontrival because neither argument is *strictly* decreasing with time, but rather they take turns decreasing. You can treat the arguments as a lexigraphic pair, or notice how their sum decreases.

gcd(a,b):
    if (a < 1 || b < 1):
        return a + b
    elsif (a < b):
        return gcd(a, b%a)
    else:
        return gcd(a%b, b)

*Case Study: Collatz Conjecture*

This is a diffcult example because it has to do with a simple recursive function. In pseudocode (untested):

# apply single round to an integer n
f(n):
if (n % 2 == 0):
return n/2
return n*3+1

# apply m rounds to integer n. Can allow in language.
g(n,m):
if (m == 0):
return n
return f(g(n,m-1))

# does it halt? Cannot be allowed in language.
h(n):
if (n == 1):
return 0
return h(f(n)) + 1

#### Data vs Codata

There is a distinction between "data" which is finite, and "codata" which is potentially infinite. Codata streams can be either externally generated (reading from an infinite stream) or internally generated by an explicit "infinite list" generator.

When there is no source of codata, the program must terminate. When there is codata, the program may run forever only if the codata is infinite. The key is to encourage a careful separation of codata sources from the bulk of the program so that it is clear what sections of the code could lead to non-termination.

Each block of code will fall into one of four categories:

1. Doesn't directly access codata streams, thus always terminates.
- Code blocks in this category can still operate on data *derived from* codata, because other external parts of the program could package up codata into finite chunks of data and call these functions with that data as an argument.
2. Does directly access codata streams, but still always terminates, even if codata is infinite.
- This category applies mainly when the codata stream comes as an infinite series of bounded-length chunks (e.g. bytes), and you want to fetch the next chunk in this stream. This category does allow *blocking*, which is when the program waits for the current chunk to be complete before continuing.
- I believe blocking is practically unavoidable when dealing with external data sources.
- Applies when chunk boundaries are guaranteed to exist: Fetching next word from a list of words.
- Perhaps all direct access to external streams should fall in Category 3, while the act of reading from internally-repackaged streams should fall in Category 2.
3. Directly accesses codata streams, always terminates, even if codata is infinite, as long as the codata is well-formed (words, lines, etc.).
- When the codata is externally-generated, it might be possible that the program does not terminate due to blocking because the codata is malformed (e.g. an infinite string with no newlines, so the end of the first line is never reached).
- The key to the category is that these functions, like `nextLine()`, can essentially be assumed to return a value, and it is very clear-cut what type of data to expect.
- When code in this category hangs (doesn't terminate), the reason must be clear and obvious, like trying to fetch the next word of a data stream not made of words.
- Applies when chunk boundaries are expected but not technically "guaranteed": fetching next word from a list of arbitrary characters.
4. Directly accesses codata streams, and might not terminate if the codata is infinite.
- example is code that terminates based on some computable property of the codata stream, but there is no way to tell if this will ever happen or if you will infinitely consume codata.
- If codata is finite, terminates at end of stream.
- The return type of these code blocks must be decidable beforehand, so that we can say "if this function terminates, it returns a variable of this type."

*Case Study: Goldbach Conjecture*

The Goldbach conjecture states that every even number greater than 2 is the sum of two primes. Determining whether or not a number is prime is primitive recursive, as is checking a single case for the conjecture. The termination status of any program that tests all even numbers one-by-one is unknown, and so any program written in this language to test the Goldbach conjecture must explicitly use an internally-generated codata stream to produce the list of even numbers to test. There will be "test case code" which is guaranteed to terminate, and "infinite stream" code with unknown termination status.

*Case Study: Hydra Game*

The [hydra game](https://slate.com/human-interest/2014/06/hydra-game-an-example-of-a-counterintuitive-mathematical-result.html) is game in which you start with a tree, and each turn you remove one leaf from the tree, but each round a large portion of the hydra regrows according to special rules. This game always terminates, no matter what finite number of copies are regenerated each time.

Consider the following program:

start with an arbitrarily-sized tree
while tree exists:
cut any leaf off
read a number from external stream
make that many new copies of the appropriate subtree
This program always terminates (ignoring minor technical issues). The code of cutting and replicating belongs in Category 1, while the program as a whole is Category 3. The use of codata is to emphasize the fact that the number of copies created at any stage can be completely arbitrary.

What will it take to make a termination checker capable of detecting this?

### No Runtime Errors

Powerful type checking and type inference.

See: liquid types, dependent types, SMT solvers, etc.

Theories of interest:
- theory of real closed fields (real numbers with addition and multiplcation)
- presburger arithmetic (natural numbers with addition only)
- theory of uninterpreted functions?
- theories of arrays, bitvectors, pointers?

Interested solely in theories that are:
- consistent
- [complete](https://en.wikipedia.org/wiki/Complete_theory) (examples from wikipedia)
- Presburger arithmetic
- The theory of [real closed fields](https://www.cl.cam.ac.uk/~jrh13/papers/cade05.pdf) - really slow proof-producing algorithm, maybe there is something faster I'm missing? Is doubly-exponential.
- [Existential theory of the reals](https://en.wikipedia.org/wiki/Existential_theory_of_the_reals) - is in PSPACE
- [all categorical theories](https://en.wikipedia.org/wiki/Categorical_theory) - higher-order categorical theories might not be decidable?
- Tarski's axioms for Euclidean geometry
- The theory of dense linear orders without endpoints
- The theory of algebraically closed fields *of a given characteristic*
- decidable
- [monadic second-order theory of the binary tree](https://en.wikipedia.org/wiki/Monadic_second-order_logic)
- [A Decision Procedure for a Sublanguage of Set
Theory Involving Monotone, Additive, and
Multiplicative Functions](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.5.2106&rep=rep1&type=pdf)
- [Decidable fragments of the Simple Theory of Types with
Infinity and NF](https://arxiv.org/pdf/1406.4384.pdf)

Theory vs Logic vs Deductive System
- theory:
- consistent: impossible to derive a contradiction
- complete: for every statement, either it or its negation is derivable from the axioms
- decidable: there exists an algorithm to determine whether or not a given statement is a theorem
- logic:
- deductive system: a notion of provability
- soundness: every provable sentence is universally valid
- completeness: every universally valid sentence is provable
- effectiveness: there exists a proof-checking algorithm that can determine if a given sequence of symbols is a valid proof

[Weak Theories and Essential Incompleteness](http://www1.cuni.cz/~svejdar/papers/sv_ybk07.pdf)

[A Decidable Fragment of Second Order Logic
With Applications to Synthesis](http://madhu.cs.illinois.edu/eqsmt-csl2018.pdf)

[First-order theories](http://theory.stanford.edu/~arbrad/slides/cs156/lec3-4.pdf)

What is temporal logic and what can we use it for?
- [A Survey on Temporal Logics](https://arxiv.org/pdf/1005.3199.pdf)
- [A Decidable Intuitionistic Temporal Logic](https://arxiv.org/pdf/1704.02847.pdf)
- [Decidable fragments of first-order temporal logics](https://spiral.imperial.ac.uk/bitstream/10044/1/624/1/hwz.pdf)
- [A deciable temporal logic of parallelism](https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1039700748)
- [Undecidability and temporal logic:
some landmarks from Turing to the present (powerpoint)](http://www.tech.dmu.ac.uk/STRL/time12/Goranko_TIME%202012-trans.pdf)
- [Safety Metric Temporal Logic is Fully Decidable](http://www.cs.ox.ac.uk/james.worrell/tacas06.pdf)
- [A Decidable Temporal Logic for Events and States](http://www.inf.brad.ac.uk/~skonur/papers/time06.pdf)
- [Alternating Time Temporal Logic](http://www.diag.uniroma1.it/bloisi/didattica/apprendimento0809/atl.pdf)
- [Extended Computation Tree Logic](https://arxiv.org/ftp/arxiv/papers/1006/1006.3709.pdf)
- CTL model-checking: P-complete
- CTL satisfiability: EXPTIME-complete
- CTL* model-checking: PSPACE-complete
- CTL* satisfiability: 2EXPTIME-complete
- CTL[VPL] is what?

"Any recursively enumerably axiomatizable theory which is complete is also decidable"

What theories are decidable *efficiently*?
- Presburger arithmetic decidability is O(2 ^ 2 ^ n) which is poor
- What can be done in P?
- What can be done in EXPTIME?

Pushing the limits of decidable type inference with [liquid intersection types](https://arxiv.org/pdf/1503.04908.pdf)?
- Hindley-Milner type inference is exponential in worst case (DEXPTIME-complete), but polynomial in expected case.
- We must be less powerful than System F because System F type inference is undecidable.
- ComplexityZoo claims that "System T" is more manageable?

What theories can be combined?
- [Combinations of theories for
decidable fragments of first-order logic](https://members.loria.fr/PFontaine/Fontaine12.pdf)
- [deciding combined theories powerpoint](http://flolac.iis.sinica.edu.tw/flolac15/_media/combination.pdf)
- [Nelson-Oppen powerpoint](https://courses.cs.washington.edu/courses/cse507/14au/slides/L7.pdf)
- needs stably infinite theories
- convex in polynomial time, nonconvex in exponential
- [combining Stoshak theories](http://www.csl.sri.com/users/rushby/rta02.pdf)
- [complexity, convexity, and combinations of theories](https://core.ac.uk/download/pdf/82156062.pdf)
- what is difference between decidability and satisfiability?
- summary of time complexities (in DNF = disjunctive normal form)
- theories of integers under addition
- Presburger: doubly exponential
- Quantifier-free Presburger DNF: NP-complete
- Quantifier-free DNF with only equalities: O(n^3)
- not convex
- rationals under addition
- Quantifier-free DNF: in P
- convex
- equality with function symbols
- Quantifier-free DNF: O(n^2)
- Satisfiability for quantifier-free: NP-complete
- convex
- list structure with `car`, `cdr`, and `cons`
- NP-complete
- different axioms with easier satisfiability complexities (linear or poly)
- convex
- arrays under selecting and storing
- NP-complete
- not convex
- integers with function symbols
- decidable
- integers and arrays
- decidable
- rationals + lists + arrays + functions
- NP-complete
- integers + arrays
- NP-complete
- integers + functions
- NP-complete

I believe the final type system will be able to detect this example of dead code:

var a,b,c = any three numbers
if (a < b) {
    if (b <= c && a >= c) {
        ... dead code ...
    }
}

### Minimal Annotations

On one extreme end is Coq, in which every program terminates, but only because every program is essentually a complete, user-written proof of correctness. We are interested in basically the opposite: The termination and typing guarantees will be a direct result of syntactic constraints on the language in combination with fully-automatic and decidable type/termination checkers. Minimal type annotations.

Generally-speaking for typical languages, the set of syntactically-correct programs is context-free, while the set of semantically-correct programs is not. (Easy example: for a program to run, variable names must be consistent across distant parts of the program, which is not checkable by a context-free grammar.) Are we limited in any way by requiring our grammar to be context-free?

Perhaps we can allow annotations in the form of optional "assert" statements which narrow down a variable's type. Then the issue is what to do if the assert is incorrect. I'm mostly interested in avoiding runtime errors as much as possible, but maybe we should allow programmers to "run the risk" if they so choose.

### Theoretical limitations

Writing a self-interpreter will be impossible.

Dealing with not-basic math functions will be difficult because of undecidability for theories involving either integers with multiplication or real numbers with trig. In these cases, the programmer will often be required to write IF-ELSE statements that help prevent divide-by-zero or null value errors.

### Stream Tokenizing

Stream tokenizing is when a stream made of smaller units is combined into bigger units.

Termination category 3 (halt on well-formed input) vs category 4 (halt on finite input) is an important division.

Regular expressions (in the formal sense) can serve as a basis for what can be considered "well-formed" input. Why regexes?
- it is decidabe whether two regexes are equivalent (undecidable for non-regular languages)
- can generate valid inputs from a regex
The aspect of invertibility means that, given input tokenizing code, it is easy to determine whether or not input is well-formed and what sorts of inputs would be considered well-formed.

### Dataflow Programming

Envision the processing of a codata stream like a an assembly line, comprised of many individual modules with multiple inputs and ouputs.

Packets can either be "pushed" or "pulled" through an assembly line.

### Subtyping and OOP

Type inference can be difficult in OOP languages. For example, the following function can accept "any object possessing x and y fields that can be added" and returns data of whatever type x+y is.

f(o):
    return o.x + o.y

This code can take on very different meanings when passed different classes of objects, so there is no guarantee that this function makes sense to apply to any particular object. Consider a class `R` where `x` and `y` are integers being added, compared to a class `L` where `x` and `y` are strings being concatenated. It might make sense to compute `f(r)` but `f(l)` could be meaningless. Also, specificity will be lost if the type-checker cannot realize that `f()` is only ever applied to `R` and not `L`.

Idea: require type annotations for objects?

Type annotations help promote safety, not safety as in not crashing, but also safety in that you are restricted to performing meaningful computations.

Key goals of objects:
- group together data fields that are typically manipulated together
- packaging functions with the data, allowing code reuse and keeping things isolated.

Key goals of subclasses and interfaces:
- allow for code reuse between similar classes
- detailing the relationships between fields of different classes so that functions can operate on broad sets of classes

*Case Study: Diamond Problem*

Consider the following classes. There exists a DAG which relates all of these classes of quadrilaterals, but (1) there are multiple paths for inheritance, and (2) there are variations in naming conventions for variables.

Parallelogram is parent class
 - long side
 - short side
 - angle
Rectangle is a Parallelogram
 - long side
 - short side
Rhombus is a Parallelogram
 - side
 - angle
Square is a Rhombus and Rectangle
 - side

paths                  s1  s2  s=  a1  a2  a=
    +    kite           w   w               w
+ +   +  trapezoid      w   w       w   w
      +  iso trap       w   w               w
+ +      parallelo      w   w               w
  + +    rhombus                w           w
+     +  rectangle      w   w
+ + + +  square                 w

### Black Box Data Structures

A black box data structure is a data structure who implementation details are unknown and inaccessible to the code that uses that data structure.

A given might implement some *interface* and make certain *promises*. An implementation of a `Set` might have an interface of `add(int):void`, `del(int):void`, and `query(int):bool`. The core "promise" would be that `query(x)` for any given `x` only returns true if it is preceded by `add(x)` without a `del(x)` in between.

#### True Black Box

A completely black box data structure makes no promises beyond simple type-safety. This means that the code cannot assume the existence of any relationship between what is written to and read from the data structure. At the same time, it is necessary to assume that the output of the structure may depend on everything.

True-black-boxing is a way to enable a program to interact with any arbitrary data structure while maintaining the guarantee of termination. It is likely the case that you could implement a data structure with difficult/undecidable theory, using this language, in which case allowing the behavior of the structure to meaningfully influence control flow leads to undecidable behavior.

### Fundamental Data Types

#### Natural Numbers and Whole Numbers

The natural numbers are all integers >= 1, and the whole numbers are all integers >= 0.

#### Integers

Might implement first and treat natural numbers as a dependent subtype.

#### Rationals?

Precise non-integers. I will probably not implement these, because I might as well go all the way to floats.

#### Floats

Imprecise non-integers. The imprecision means that there must be additional limits on the extent to which floating point calculations can influence control flow.

#### Strings

Can be concatenated, has length, can match regular expressions(?), can replace substrings(?).

#### Lists?

#### Maps?

#### Arrays?

[What’s Decidable About Arrays?](http://theory.stanford.edu/~arbrad/papers/slides_arrays.pdf) and [paper](http://theory.stanford.edu/~arbrad/papers/arrays.pdf)

[other work by Aaron Bradley](http://theory.stanford.edu/~arbrad/pubs.html)

#### Sets?

#### Matrices?

[decidable 2x2 matrix semigroup membership](https://pdfs.semanticscholar.org/0595/3c0e69ecce1c107f21c93a629e369f3509dd.pdf)
[decidable mortality for pair of 2x2 matrices](https://hal.inria.fr/inria-00073848/document)
[powerpoint of other problems](https://personalpages.manchester.ac.uk/staff/Mark.Kambites/events/nbsan/nbsan20_bell.pdf)

### Information Channels

Precisely limit what properties of what variables have what degree of influence over control flow. There must be no information back/side channels.