Notes-on-laziness

Some notes:
------------

A fundamental assumption: 
--------------------------
All functions in the programs must terminate when lazy invocations are treated as eager invocation.
Otherwise, we report that there could be infinite streams.

Need to Prove
-------------
How will this enforce the termination of all functions after the translation ?
This will also ensure that all streams in the program are finite.

Claim 1:
--------
Since all closures are created by the functions in the program, we have a global
invariant that whenever we force a value the resulting value cannot be the same 
as the original value. 
Proof: 
(a) since the value is forced it must be a closure with some arguments
(b) if we get back an identical closure with the same arguments then it means
we have a recursion the function that corresponds to the the lazy closure,
and the recursive calls happens with the same set of arguments.
Which means it is non-terminating when lazy is treated as eager

Claim 2:
--------
When we force a value it creates some more closures, one of which could again be forced
returning another closure and so on. Let R(C, n) denote a predicate that 
is true if after forcing closure C, and a closure resulting from C and so on 'n' 
times, we still have a closure.
We have a invaraint that: \exists n \in nat s.t. ~R(C, n).

Alternatively, we can show that every cycle in the transformed program corresponds to a cycle in the
input program, but this may also be hard. Since cycle could be offesetted as the recursive 
calls are invoked at different points in the program.


Important regarding termination
--------------------------------
Despite this, in the translation the functions may not terminate on all inputs since there is global
invariants are not enforced. So how do we make sure that all functions after 
translation do terminate.

One way to handle this would be to change the model and create a new free variable for the result and 
then relate the result and the function in eval, which is like an assumption on the input (a precondition).
(We know that the precondition is satisfiable because it is for the data-structures created in the program.)

However, we somehow need unlimited supply of free variable of a type. 
To do that we can have a free-list of free-variables as arguments 
(similar to the oracle strategy for non-determinism).
For eg. sealed abstract class FreeList
	case class Nil() FreeList
	case class Data(fl: FreeList) extends FreeList // returns the data component
	case class Next(fl: FreeList) extends FreeList

define a function 'nextFree' : FreeList -> FreeList. 
var count = 0
nextFree(l) =
  count += 1
  Data(l :/ (1 to count - 1){ (acc, _) => Next(l) })

Everytime we call a function within the body we case use nextFree(l), where l is the input free-list,
  to get a new free-list.
We can now add uninterpreted functions that would map the free-list to a desired value,
for instance, to an ui result of a required type, or to a fresh-integer that denotes 
fresh-ids.


Important: Reasons for unsoundness
--------------------------------------

a) the assertion on the newC function that the new closure is unevaluated may result in unsoundness
	- fix: create new identifiers at the time of creating functions. We can also try and use epsilons.

b) Normal data-types can help ensure acyclicity and finiteness of stream but that means we need to create 
   free variables at the time of creation
	currently, we are creating axioms that state acyclicity.

Benchmarks to think about
--------------------------

1. Lazy constraint solving 	
	We can get demand driven pointer-analysis. Can we prove its running time ?

2. Packrat parsers uses memoization
	Can we prove its running time ?

3. ConcTrees full version ?

4. Binomial heaps ?

5. Futures: How about redex algorithms or map-reduce algorithms ?

Things to implement:
----------------------

a) A way to check monotonicity of preconditions
b) Use monotonicity while checking proofs
c) Automatically synthesize the invariant that the state is preserved
d) We can always assume that state is monotonic which proving the specs
c) Extensions for futures 
d) Extensions for memoization
e) Extending Orb for type parameters
*f) Try to separate the instrumentation for state and value, if not add a postcondition
   that the value part of the state-instrumented program is same as some function that does not use state.
   But, how can we do that ?

Integration

Try to fix bugs in CVC4 proof and also try to integerate it with the system
Try to integrate the tool with Orb

Some Notes
----------

a) It is very essential to make the separation between value and state component explicit
	we can use something like: "foo(x, uiState())" and "foo(x, st)" where st is the actual input state.

b) We need to treat Lazyarg's as not closures. That is, they don't change state and are not considered as Unevaluated. They
	are never added to the set. 
	We can have an implicit type conversion from normal values to lazyargs. 
	Since normal values are eagerly computed. This lets us specify lazyargs succinctly in the code.
	We need to change isEvaluated and value function call modelling

c) Futures when modelled as closures can be stored and then later joined. 
e.g. a function  'spawn' that will spawn tasks and a function 'join' that will join 
the spawned threads.
However, we need to explicitly mark the functions that can be executed in parallel from the 
point of creation of a Future to the point of joining the Future.
Eg. as 
spawn()
spawn()
parallel(op(), join(), join())
//this means op() and the two futures will execute in parallel.

d) Memoization: They are evaluated at the time of creation unlike lazy closures. 
		We need to track whether a closure belongs to a state or not.