-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlog.txt
174 lines (119 loc) · 5.95 KB
/
log.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
2015-06-09: The code in nonmonadic/ was originally based on what has now become
https://github.com/nicolabotta/SeqDecProbs/tree/master/manuscripts/2014.LMCS/code/DynamicProgramming
in particular the S12* files (the time-parameterised, non-monadic
case).
Later this Agda code has been the intermediate step towards a
re-implementation in Idris for the Avoidability theory paper:
https://github.com/nicolabotta/SeqDecProbs/blob/master/manuscripts/2015.MSS/code/monadic.lidr
This also led to further changes in the Idris code base, now developed in
https://github.com/nicolabotta/SeqDecProbs/tree/master/frameworks/14-
This Idris code base is partially mirrored in Agda in this repository under
https://github.com/patrikja/SeqDecProb_Agda/tree/master/libs
2015-03-09: Split off from larger local repo and pushed to github
This Agda development was an attempt at understanding the Idris code
in what later became https://github.com/nicolabotta/SeqDecProbs
The code is for the time-parameterised, non-monadic case.
Upgraded agda-stdlib to version 0.9 to match with Agda-2.4.2.2.
2014-09-06: Installed new Agda: version 2.4.2
cd ~/lib
wget https://github.com/agda/agda-stdlib/archive/v0.8.1.tar.gz
tar -zxf v0.8.1.tar.gz
rm agda-stdlib
ln -s agda-stdlib-0.8.1/src agda-stdlib
agda -i . -i /home/patrikj/lib/agda-stdlib Examples.agda
-> loads fine, but lots of holes (metavariables) remain
2014-04-30: Looking at the Agda code again
log.txt -- this documentation file
Blt.agda -- Helper: bounded natural numbers (Fin)
Prelude.agda
Max.agda -- parts of the assumptions would fit in here (not used by Context yet)
Context.agda -- records of assumptions for the main algorithm
OptimalControls.agda -- imports Context
OptimalPolicies.agda -- imports Context
BackwardsInduction.agda -- Main file
Examples.agda -- Imports most of the other files
Controls.agda -- TODO - still Idris code (imports Context)
2013-11-04: Paper submitted [was later rejected]
Dear Patrik Jansson,
Nicola Botta <[email protected]> submitted the following
paper to Do-Form@MCS2014:
-------------------------------
Sequential decision problems, dependent types and generic solutions
-------------------------------
You are listed as one of the authors of
this paper. To enter the Do-Form@MCS2014 Web
pages you should visit
https://www.easychair.org/conferences/?conf=doformmcs2014
and enter your EasyChair user name and
password.
If you forgot your user name or password,
please visit
https://www.easychair.org/account/forgot.cgi
and specify [email protected] as your email address.
Best regards,
EasyChair Messenger.
2013-10-25: Three TODOs done - just OptLemma remaining
2013-10-25: remaining TODOs are
Context.agda:
* use the Max record in Context (not important)
BackwardsInduction.agda:
* define OptLemma based on the time-independent case
* optExtension: calculates an optimal Policy to extend a PolicySeq with. ***TODO: complete definition
* OptExtensionLemma: proces that optExtension really does what it should. ***TODO: complete proof
----------------------------------------------------------------
Discussion:
* Differences in readability of definitions
** Idris has shorter type signatures where certain parameters can be elided
** Agda has very nice syntax for equality proofs
----------------------------------------------------------------
I take a snapshop of the directory for sending a bug report later.
../SeqDecProb_2013-10-25_record_bug.tgz
Bug in Agda version 2.3.2:
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Records.hs:216
To reproduce:
Load the file BackwardsInduction.agda
Script version:
tar -zxf SeqDecProb_2013-10-25_record_bug.tgz
cd SeqDecProb
agda -i ~/lib/agda-stdlib -i . BackwardsInduction.agda
2013-10-25: Continuing the development
Step 1: Identify the current state and dependencies
Five working modules in dependency order:
* Prelude: [OK] (minimal)
* Context: [OK]
* OptimalControls: Prelude, Context [OK]
* OptimalPolicies: Prelude, Context, OptimalControls [OK]
* BackwardsInduction: Prelude, Context, OptimalPolicies [OK]
One module with unconverted Idris-code:
* Controls: TODO: convert from Idris
Step 2: Short summary of the modules
Prelude: useful definitions collected + some Idris terminology
* Nat, Unit, Product, PropositionalEquality and Type = Set
Context: collects the assumptions used in the rest of the development
* record Max A Reward ... -- for types we can find the maximum of a function from A to Reward
* record RewProp -- properties for the Reward type (think: real numbers)
* record Context -- parametrised record collecting requirements for backwards induction
** TODO: use the Max record in Context (not important)
OptimalControls:
* XV t n -- subset of viable X
* CtrlSeq x n -- a control path from x of length n
* viableLemma -- CtrlSeq x n -> viable n x
* val ~: CtrlSeq x n -> carrier
* OptCtrlSeq -- defines optimality of control sequences
OptimalPolicies:
* Policy t n is a function from X that generates a "viable" y
* PolicySeq t n -- a sequence of policies for n steps from t
* ctrls ~: PolicySeq t n -> CtrlSeq x n
* Val ~: PolicySeq t n -> carrier
* OptPolicySeq -- the concept of optimality for PolicySeq
* OptLemma: ***TODO: define this based on the time-independent case
BackwardsInduction:
* OptExtension: a relation stating when a PolicySeq can be extended by a certain Policy
* valY: the value of a step + the rest of a PolicySeq
* optExtension: calculates an optimal Policy to extend a PolicySeq with. ***TODO: complete definition
* OptExtensionLemma: proces that optExtension really does what it should. ***TODO: complete proof
* Bellman: the step case in the proof of backwards induction
* backwardsInduction: recursively build a PolicySeq
* BackwardsInductionLemma: correctness of backwardsInduction
----------------