Static Analysis

Techniques

https://en.wikipedia.org/wiki/Static_program_analysis

https://en.wikipedia.org/wiki/Category:Static_program_analysis

Type Inference

https://eli.thegreenplace.net/2018/type-inference/

Escape Analysis

https://en.wikipedia.org/wiki/Escape_analysis

Control Flow Analysis

https://en.wikipedia.org/wiki/Control_flow_analysis

http://www.ccs.neu.edu/home/shivers/papers/diss.pdf

http://haskell.cs.yale.edu/wp-content/uploads/2011/02/Orbit.pdf

https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf?from=https%3A%2F%2Fresearch.microsoft.com%2F%7Eakenn%2Fsml%2FCompilingWithContinuationsContinued.pdf

Termination Analysis

In general: proof every recursive function has a well-founded relation < such that a_n+1 < a_n where a are the succesive arguments to recursive calls.

Walther Recursion is a more powerful generalization of primitive recursion, it always terminates, but is more expressive. http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/On-proving-termination-AIJ-71-1_1994-2.pdf

Example: flow graph for facts

fact n return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 m: fact m step2
        step2 f: mul n f return

We would like to prove:

fact => return

Meaning: fact will either diverge or eventually call return.

Proof by induction:

Base case (no recursion): Every path either recurses or ends in return.

fact -> isZero -> base -> return
fact -> isZero -> recurse -> sub -> step1 -> fact

Inductive case. Assume fact -> return for n recursions. Show that this holds after one more recursion.

fact -> isZero -> base -> return
fact -> isZero -> recurse -> sub -> step1 -> fact -> step2 -> mul -> return

This analysis can probably be done fully automated. TODO: check cases of mutual recursion and recursive functions that have multiple exit points.

Example: flow graph for isEven

isEven n then else: isZero n then step
    step: sub n 1 recurse
    recurse m: isEven m else then

isEven -> isZero -> then
isEven -> isZero -> step -> sub -> recurse -> isEven

Try isEven => then:

isEven -> isZero -> then
isEven -> isZero -> step -> sub -> recurse -> isEven -> else

False. Try isEven => then, isEven => else

isEven -> isZero -> then
isEven -> isZero -> step -> sub -> recurse -> isEven -> else
isEven -> isZero -> step -> sub -> recurse -> isEven -> then

Proven.

Example closures for fact

fact n return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 m: fact m step2
        step2 f: mul n f return

main return1: fact 5 m0
    m0 f: print f m1
    m1: return1

Create a map from names to call symbols sets:

fact: { isZero n base recurse }
base: { return 1 }
recurse: { sub n 1 step1 }
step1: { fact m step2 }
step2: { mul n f return }
main: { fact 5 m0 }
m0: { print f m1 }
m1: { return1 }

Remove builtins:

fact: { n base recurse }
base: { return }
recurse: { n step1 }
step1: { fact m step2 }
step2: { n f return }
main: { fact m0 }
m0: { f m1 }
m1: { return1 }

Remove own arguments:

fact: { base recurse }
base: { return }
recurse: { n step1 }
step1: { fact m step2 }
step2: { n f return }
main: { fact m0 }
m0: { m1 }
m1: { return1 }

Replace names by their call, while removing own arguments:

fact: { }
base: { return }
recurse: { return n }
step1: { return n }
step2: { return n }
main: { base recurse m0 }
m0: { m1 }
m1: { return1 }

We now have a list of closure parameters.

We can turn this into a domination graph by replacing parameters by their procedures:

fact:
base: { fact }
recurse: { fact }
step1: { fact }
step2: { fact }

Example closure elimination for fact

fact n return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 m: fact m step2
        step2 f: mul n f return

Add closure values as parameters

isZero' n base recurse return n
sub' a b k return n

fact n return: isZero' n base recurse return n
    base return: return 1
    recurse return n: sub' n 1 step1 return n
        step1 m return n: fact' m step2 return n
        step2 f return n: mul n f return

We need to modify builtins to pass parameters along. Not elegant, but doable. But then we need to do the same transform to fact' and then we are at square one again, needing a fact''. We are essentially building a stack, which we want to avoid.

What should the ideal result look like?

First, make it a proper tail call. How we do this is a different discussion.

fact n return: fact' n 1 return

fact' n a return: isZero n base recurse
    base: return 1
    recurse: sub n 1 step1
        step1 n': mul n a step2
        step2 a': fact' n' a' return

Now try the same procedure again:

fact n return: fact' n 1 return

fact' n a return: isZero' n base recurse n a return
    base n a return: return 1
    recurse n a return: sub' n 1 step1 n a return
        step1 n' n a return: mul' n a step2 n' return
        step2 a' n' return: fact' n' a' return

We still need modified version of the built-ins that pass parameters along, but we no longer need to recursively transfor fact itself.