@@ -8,42 +8,55 @@ type-checking can be found below.

###### Framework and proofs

*[Framework](Framework.lidr): Contains the lightweight version of the BJI-framework and its extension (as described in section 3 and 4), the proof of the correctness result from (section 6), and proofs of the auxiliary results (section 6 and appendix).

*[Framework](Framework.lidr): Contains the lightweight version of the

BJI-framework and its extension (as described in section 3 and 4),

the proof of the correctness result from (section 6), and proofs of the

auxiliary results (section 6 and appendix).

###### Examples and proofs for specific instances

*[List](List.lidr): Contains proofs for a non-deterministic instance of the framework in which the monad `M` is instantiated with `List`.

*[List](List.lidr): Contains proofs for a non-deterministic

instance of the framework in which the monad `M` is instantiated

with `List`.

*[Id](Id.lidr): Contains proofs for a deterministic

instance of the framework in which the monad `M` is instantiated as identity functor.

instance of the framework in which the monad `M` is instantiated

as identity functor.

*[MaxList](MaxList.lidr): Contains the proofs for an example measure that fulfills all three requirements.

*[MaxList](MaxList.lidr): Contains the proofs for an example measure

that fulfills all three requirements.

*[ListMeasures](ListMeasures.lidr): Contains the proofs for the abstract `List` measures discussed in section 5.3.

*[ListMeasures](ListMeasures.lidr): Contains the proofs for the

abstract |List| measures discussed in section 5.3.

*[GoodBadExample](GoodBadExample.lidr): Contains the formalization of the example of section 2.1.

*[GoodBadExample](GoodBadExample.lidr): Contains the formalization of

the example of section 2.1.

*[SchedulingExample](SchedulingExample.lidr): Contains the formalization of the example of section 2.2.

*[SchedulingExampleVariant1](SchedulingExampleVariant1.lidr): Contains a

simple possible formalization of the example of section 2.2.

*[GoodBadCounterExamples](GoodBadCounterExamples.lidr): Contains some of the counter-examples to `valMeasTotalReward` of section 5.2.

*[SchedulingExampleVariant2](SchedulingExampleVariant2.lidr): Contains a

possible formalization of the example of section 2.2 that makes more use

of type dependency.

*[GoodBadCounterExamples](GoodBadCounterExamples.lidr): Contains some of the

counter-examples to valMeasTotalReward of section 5.2.

###### Auxiliary Definitions

*[Equality](Equality.lidr): Definition of extensional equality as in [2].

*[Sigma](Sigma.lidr): Definition of Sigma types as in [2].

#### Type-Checking Instructions

The following has been successfully tested using Idris version 1.3.2:

* The source files can be typechecked all at once with

`idris --checkpkg code.ipkg`

`idris --checkpkg valval.ipkg`

or built with

`idris --build code.ipkg`

`idris --build valval.ipkg`

* Individual files can be loaded into the Idris REPL using

...

...

@@ -51,7 +64,7 @@ The following has been successfully tested using Idris version 1.3.2:

* Generated intermediate code and executables can be deleted with

`idris --clean code.ipkg`

`idris --clean valval.ipkg`

## References

...

...

@@ -61,5 +74,5 @@ Backward Induction. *submitted to J. Funct. Program*.

[2] Botta, N. (2016-2021). [IdrisLibs](https://gitlab.pik-potsdam.de/botta/IdrisLibs).

[3] Botta, N., Jansson, P., Ionescu, C. (2017). Contributions to a computational theory of policy

advice and avoidability. J. Funct. Program. 27:e23.

[3] Botta, N., Jansson, P., Ionescu, C. (2017). [Contributions to a computational theory of policy

advice and avoidability](https://doi.org/10.1017/S0956796817000156). J. Funct. Program. 27:e23.