-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdeveloper_notes.txt
84 lines (52 loc) · 2.5 KB
/
developer_notes.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
***** Notes *****
***Stuff to maintain project:***
To generate documentation:
cabal configure
cabal haddock --hyperlink-source
Doing this checks for compilation errors, so it's a good way to check everything 'works' somewhat.
git commands:
git status
git add
git commit -m
git push
to draw graphs:
dot -Tpdf GraphDrawingOutput.gv -o GraphDrawingOutput.pdf
*** Notes on packages used ***
newtype:
wrapping and unwrapping Newtypes.
set-monad:
using Sets as Monads.
***** Todo *****
*** Display ***
> Pretty print sets
* Graph Drawing *
Make 'pass forward my name' rather than 'request backward for my name' --> DONE
*** LDL to AFA ***
> make LDLogicNNF datatype
*** Automata ***
> Make versions of translations with reachability.
n2d = n2dNaive
n2d = n2dReachable
This is proving a bit hard to make work... Or rather opaque.
> A possible (experimental) reformulation: Automata are things which can be *queried*.
What is the initial state, is this a final state, what is the transition on this etc.What I have now, where these items are explicitly stored, is just one implementation of that. More generally, those things could be ready to be computed but not actually computed. i.e. lazy. Algorithms which work on automata, use them to search a state space (including translations between automata themselves). Translated automata then just do compositions of these queries. Of course, they could be 'realised' into actual state...
Something like this:
class (FAquery q a r) m where
alpha :: a -> m -> Bool
state :: q -> m -> Bool
init :: m -> q
transition :: q -> a -> m -> r
final :: q -> m -> Bool
a2n :: ((FAquery q a (BasicPropLogic q) m), (FAquery q a (S.Set q) n)) => m -> n
a2n afa =
blah blah blah
> I'm starting to think there's no point in having "DFAs" at all, since there is no guarantee in practical programming of having the transition function be a total function anyways. --> We can weaken the notion of DFA to have partial functions. At least a partial function is not a general relation.
*** Graph Algorithms ***
NFA emptiness --> Actually for any AFA A, you can just inspect the final set state of a2nreach A...
*** LDL to AFA ***
Write the translation:
did some NNF stuff... almost ready to put in the transition function of the AFA...
I wonder, perhaps the AFA -> NFA -> DFA all work properly? It all hinges on 'reach'.
I need to actually test these things. Well, I tested NFA -> DFA with reach, which works well.
*** Logic & Dependents ***
Change Prog to Reg --> DONE