features-and-implementation3 (5999B)
1 * Invariants 2 * Scope of the invariants: 3 * Input contracts, types and structural properties 4 * Output contracts, types and structural properties 5 * Transformation invariants (relate the input and output graphs) 6 * Time of verification: 7 * Run-time 8 Should be easy enough to implement: Add a define-graph-invariant form, recognize these options, and check 9 them at run-time. Implemented as some sorts of contracts. 10 * Compile-time 11 * Node types 12 * Statically-enforced structural invariants at the level of node types 13 (e.g. disallow cycles in the types, to ensure there are no cycles in the instance) 14 * Macros can be used to generate code which is known to be correct 15 e.g. paths 16 * Concern: static "by construction" guarantees may interfere with each other, if they fill in some nodes, 17 e.g. a "no cycles starting from this node" constraint would not work as expected if a "backwards link" 18 is filled in afterwards. We probably need to hardcode a set of constraints which know about eachother 19 and about the potential interactions. 20 * Conserve well-scopedness within a transition: pass in nodes flagged with a ∀ type, and check 21 that the output contains that flag. Potentially out-of-scope fields in the input do not have the flag. 22 * PHOAS 23 * Specification 24 * Invariants specified in the graph type 25 * Transformation invariants specified on the graph creation code 26 * Checks (run-time or the various compile-time mechanisms) are specified in the graph creation code 27 The graph creation code must enforce all invariants within the type 28 That way, it is guaranteed that any instance of the graph type satisfies its invariants, either by 29 construction, or as a guard at the end of the construction. 30 31 ; The body should produce a function of type (→ (Listof Nodeᵢ) … Boolean) 32 ; The body should also return an indication about which invariants it ensures. Maybe use {~seq #:ensures (invariant-name inariant-arg …)} … 33 however this does not allow the body to perform some minimal amount of rewriting on the "ensures" options. 34 (define-syntax/parse (define-graph-contract (name g-descriptor arg …) . body) 35 #'(define-syntax name 36 (graph-contract 37 (λ (g-descriptor arg …) . body)))) 38 39 ;; TODO: find a way to translate this to a type, with subtyping for weaker invariants. 40 ;; The type only serves to testify that the invariant was statically enforced or dynamically checked at construction, it does not actually encode the property using the type system. 41 (struct invariants-wrapper ()) ;; Use a private struct to prevent forging of the invariants aggregated in a case→ (since it is never executed, any non-terminating λ could otherwise be supplied). 42 (define-for-syntax invariant-introducer 43 (make-syntax-introducer)) 44 ;; the body should return the syntax for a type, such that less precise invariants are supertypes of that type. 45 (define-syntax/parse (define-graph-invariant (name g-descriptor arg …) . body) 46 #'(define-syntax name 47 (graph-invariant 48 (λ (g-descriptor arg …) . body)))) 49 50 The type of a graph node with the invariants inv₁ … invₙ on the graph must include an extra dummy field with type 51 (invariants-wrapper 52 (case (→ inv₁ inv-arg … #t) 53 … 54 (→ invₙ inv-arg … #t))) 55 56 The invariant arguments can be symbols, to indicate node types or field names. 57 58 Concern: invariants on a graph may not have the same semantics if the graph has more or fewer nodes? 59 60 * Automatic generation of mappings 61 * when there is no mapping taking an old node as an input, a mapping is automatically generated. 62 The mapping simply translates the old node to the new node type, and recursively transforms its fields, 63 traversing lists etc. 64 * When there is a mapping with more than one argument, then no mapping is auto-generated for that input node type, 65 and instead calls to the mapping must be explicit (i.e. can't return the old node type). 66 * This means that we have a mechanism before the actual core graph macro, which checks and decides which mappings 67 to auto-generate. 68 * We also have a mechanism for auto-calling transformations on input node types 69 * Possibility to escape this, in order to actually insert a reference to the old graph? 70 * Some notation in the type, to indicate that the output should be an "old" node here 71 * In the rare case where we have an (U (Old nd) nd), in the mapping use some (old v) wrapper 72 indicating that the returned it should merely be unwrapped, not processed. 73 74 (define-syntax define-graph-type 75 (syntax-parser 76 [(_ _name [_nodeᵢ [_fieldᵢⱼ :colon _τᵢⱼ] …] …) 77 ;; save the graph type metadata 78 ])) 79 80 (define-syntax define-graph-transformer 81 (syntax-parser 82 [(_ _name graph-type) 83 ;; TODO 84 ])) 85 86 * Structural node equality 87 * Would be nice to coalesce nodes which are equal? (i.e. hash consing) 88 so that any two nodes which are equal? within the same graph have the same index. 89 I suppose this would be rather costly: O(n log n) comparisons, with each comparison potentially 90 costly, in principle. If we cached results, we could achieve a better run-time in practice, and 91 perhaps a better theoretical complexity if we handled cycles ourselves. 92 * The general algorithm when there are no unordered sets is deterministic finite automaton minimization 93 * The general algorithm when there are unordered sets is nondeterministic finite automaton minimization 94 * We could cache all calls to equal? on two nodes for a limited dynamic scope. 95 * If we have this, then we can, for comparisons within the same graph, quickly return #t or #f based on eq? 96 97 * Coloring: the existing graph library for Racket has some coloring algorithms: 98 http://docs.racket-lang.org/graph/index.html#%28def._%28%28lib._graph%2Fmain..rkt%29._coloring%2Fgreedy%29%29 99 Maybe we can build a wrapper for those?