Learning.Transformation

1module Learning.Transformation
2
3import Std.Foundation
4import Representation.Schema
5
6family LearningTransformation : Type 0
7constructor ReverseDifferentiation
8constructor RegisteredDerivative
9field unrestricted registeredDerivativeComponent : (family ParameterIdentity)
10field unrestricted registeredDerivativeIdentity : Bytes
11field unrestricted registeredDerivativeConformanceTest : Bytes
12constructor LocalUpdate
13constructor StateEvolution
14end-family
15
16family LearningIncompatibility : Type 0
17constructor LearningRepresentationMismatch
18constructor LearningEffectMismatch
19constructor LearningResourceMismatch
20constructor LearningTimingMismatch
21end-family
22
23-- Compatibility is structured evidence supplied by composition. Keeping the
24-- four dimensions separate makes unsupported cases visible and testable.
25family LearningCompatibility : Type 0
26constructor LearningCompatibilityOf
27field unrestricted learningRepresentationCompatible : (family StdBool)
28field unrestricted learningEffectsCompatible : (family StdBool)
29field unrestricted learningResourcesCompatible : (family StdBool)
30field unrestricted learningTimingCompatible : (family StdBool)
31end-family
32
33def learningCompositionFailure =
34  (lambda unrestricted problem : (family LearningIncompatibility) .
35    (lambda unrestricted transformation : (family LearningTransformation) .
36      (constructor StdResult StdFailure
37        (family LearningIncompatibility) (family LearningTransformation) problem)))
38
39-- Every learning mode uses the same composition boundary. The result names the
40-- first incompatible contract dimension instead of silently selecting a path.
41def composeLearningTransformation =
42  (lambda unrestricted transformation : (family LearningTransformation) .
43    (lambda unrestricted compatibility : (family LearningCompatibility) .
44      (eliminate LearningCompatibility
45        (lambda unrestricted current : (family LearningCompatibility) .
46          (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
47        compatibility
48        (branch LearningCompatibilityOf representation effects resources timing .
49          (eliminate StdBool
50            (lambda unrestricted current : (family StdBool) .
51              (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
52            representation
53            (branch StdTrue .
54              (eliminate StdBool
55                (lambda unrestricted current : (family StdBool) .
56                  (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
57                effects
58                (branch StdTrue .
59                  (eliminate StdBool
60                    (lambda unrestricted current : (family StdBool) .
61                      (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
62                    resources
63                    (branch StdTrue .
64                      (eliminate StdBool
65                        (lambda unrestricted current : (family StdBool) .
66                          (family StdResult (family LearningIncompatibility) (family LearningTransformation)))
67                        timing
68                        (branch StdTrue .
69                          (constructor StdResult StdSuccess
70                            (family LearningIncompatibility) (family LearningTransformation)
71                            transformation))
72                        (branch StdFalse .
73                          (learningCompositionFailure
74                            (constructor LearningIncompatibility LearningTimingMismatch)
75                            transformation))))
76                    (branch StdFalse .
77                      (learningCompositionFailure
78                        (constructor LearningIncompatibility LearningResourceMismatch)
79                        transformation))))
80                (branch StdFalse .
81                  (learningCompositionFailure
82                    (constructor LearningIncompatibility LearningEffectMismatch)
83                    transformation))))
84            (branch StdFalse .
85              (learningCompositionFailure
86                (constructor LearningIncompatibility LearningRepresentationMismatch)
87                transformation)))))))
88
89def learningCompositionCode =
90  (lambda unrestricted result :
91      (family StdResult (family LearningIncompatibility) (family LearningTransformation)) .
92    (eliminate StdResult
93      (lambda unrestricted current :
94        (family StdResult (family LearningIncompatibility) (family LearningTransformation)) . Nat)
95      result
96      (branch StdFailure problem .
97        (eliminate LearningIncompatibility
98          (lambda unrestricted current : (family LearningIncompatibility) . Nat)
99          problem
100          (branch LearningRepresentationMismatch . (succ zero))
101          (branch LearningEffectMismatch . (succ (succ zero)))
102          (branch LearningResourceMismatch . (succ (succ (succ zero))))
103          (branch LearningTimingMismatch . (succ (succ (succ (succ zero)))))))
104      (branch StdSuccess value . zero)))