Balisage Paper: Application of Brzozowski Derivatives to JSON Schema Validation

Mapping

Mapping performs two operations: mapping type properties to faceted types, and mapping compositional properties to extended regular expressions. We will denote this with two separate functions, μ and μM respectively. To complete the picture, we will also need a function that provides the type with its name, and a lookup function that can obtain the facets for a given named type. I use the form f(A) => B to say that the definition of the result of applying function f to A is B.

The type mapping function is fairly straightforward, although capturing the interactions with the compositional properties gets a little messy in a functional paradigm. In the formulation here, the extended regular expressions from μM are expressed as the output for a particular property (model) in the output of μ.

For the most part type properties in the schema map directly to facets in the type. If there is a type property in the schema, its value will constrain which properties map to facets; if it is an array of values, we will treat this as creating a content model disjunction between the alternatives; and if it is absent we will treat this as creating a content model disjunction between all^[4] alternatives (array, object, number, string, boolean, null). Each alternative will only gather properties relevant for that specific type value.

In what follows, P is a map of property-value pairs {p1:v1,...,pn:vn} where each property name is unique and the + operator performs a union of maps. The rules are generally written so that the set of property names is disjoint.^[5] In addition, s1, s2, etc. refer to (sub)schemas.

The definition below shows the mapping, broken down for each of the distinct type values. Most properties can be mapped independently, although there are some exceptions. That is, unless specified otherwise: μ({p:v,P}) => μ({p:v})+μ(P) and similarly μM({p:v,P}) => μM({p,v})+μM(P). Where there is a rule for a specific combination of properties, that rule takes precedence. There are a few edges cases to take care of: boolean schemas and $ref dereferencing.

It will be useful to define some standard bundles of properties. The function relevant(P,kind) will return just the properties listed for the specific kind from the map of property-value pairs. For example, relevant({minLength:1,maximum:12},"string") is {minLength:1}:

First, we define how some edge cases are handled:

The boolean schemas map to true or empty set as appropriate, and references map to the referenced definition. Specifying the details of how the JSON path gets dereferenced is beyond the scope of this paper. In what follows assume we have a fully dereferenced schema in hand.^[6] We are also assuming the schema as a whole (including the references) is valid.

The type property is the main driver for the mapping. In general it gets mapped to a kind facet plus a simpleType facet for references to simple values and occasionally other facets as well. The type names have the same meaning as in XSD2. Here are the rules for mapping the type property:^[7]

The enum and const properties apply to all kinds of values:

The string-specific properties are minLength, maxLength, and pattern

Here are the numeric property mappings:

Type properties for objects:^[8]

Array properties:

Before we get to model mapping, we need to introduce some additional notation. The notation is similar to Sperberg-McQueen05, which is a little different from Brzozowski64, but with a few alterations and extensions. JSON Schema does not need general occurrence counts, and the wildcards required are relative to a set of property names, not namespaces.

The type marking, exclusive or, conditional, simultaneous, and wildcards are extensions. Negation is present in Brzozowski64 although with a slightly different notation.

It may seem that F&G and <F,G> mean the same thing, but the difference will become clearer when we get to the definition of derivatives, because F&G matches F and G against different segments of the input, whereas with <F,G> matches F and G against the same segment of the input simultaneously. For example, a@T & a@S can never be satisfied because each symbol is unique in a JSON object so there can only be one a matched, but <a@T, a@S> may well be satisfied if both type constraints are satisfied on the value of property a.

The mapping of the basic composition operators is fairly direct:

Mapping of the object-related compositional properties requires dealing with the interactions and dependencies between them. The two main compositional properties are properties and patternProperties. Each of these consists of a set of keys and an associated schema for each key. In the case of properties the key is the property name to match in the instance; in the case of patternProperties the key is a regular expression that matches the name of the property in the instance. All properties named are optional unless their name appears in the required array. Properties otherwise unaccounted for must conform to the schema given for additionalProperties, which defaults to the true schema if absent.

To simplify things somewhat, let's first ensure that when the additionalProperties property was not specified, we treat it as an explicit true schema, that is, that all additional properties are OK. We also want to normalize the additionalProperties property when it is the false schema to remove it, and to normalize the properties and patternProperties properties to replace absence with an empty object, and the required property to replace absence with an empty array. Assume the following normalizations apply one after another:

This leaves us with two variations to map: the bundle of properties P with the properties named properties, patternProperties, and required, and the bundle of properties with those plus the property named additionalProperties as well. In either case, the mapping creates a model property with the property bundle mapped by μM: {model: μM(P)}.

Capturing the semantics of additionalProperties requires some trickiness, because if its value is not the false schema, then it applies to any properties that are not named in properties and that do not match a pattern in patternProperties. We capture this in the wildcard which takes those properties and patterns as its sets. We also capture the required property by marking appropriate properties as optional or not in the model. This is an optimization: we could instead have a simultaneous compositor where one branch handles the required properties and the other handles the type information. Both branches end up being relatively weak, in general.

The semantics of patternProperties is particularly tricky:

In general, every property listed is optional, unless it is specifically mentioned in the required array. To capture the semantics of required in an effective way is a little awkward to express algebraically. Note that it is perfectly acceptable in JSON Schema for a property to be in the required array but not mentioned by either the properties or patternProperties.

For example the following schema is perfectly OK, and will not match an object {"c":1,"dd":2} as it lacks the required a and b properties:

{
  "type": "object",
  "required": ["a","b"],
  "properties": {
    "c": { "type": "number" }
   },
  "patternProperties": {
    "d+": { "type": "number" }
  },
  "additionalProperties": true
}
        

With all that said, the general rules for mapping the object-related composition properties are:

{
  properties: {p1:s1,...pm:sm},
  patternProperties: {r1:pt1,...,ro:pto},
  additionalProperties:sp,
  required:[rq1,...,rqn]
}

    < 
      (q1@κ(t1) & ... & qk@κ(tk) & 
       ql@κ(ql)? & ... & qm@κ(tm)? &
       u1@κ(sp) & ... & uv@κ(sp) & 
       (wc(-[p1,...,pm],-[r1,...,ro])@κ(sp)|
        wc(-[p1,...,pm],+[r1,...,ro]))*
      ),
      (wc(r1)@κ(pt1) | wc(-[],-[r1]))*,
      (wc(r2)@κ(pt2) | wc(-[],-[r2]))*,
        ...
      (wc(rn)@κ(pto) | wc(-[],-[ro]))*
    >
  

{
  properties: {p1:s1,...pm:sm},
  patternProperties: {r1:pt1,...,ro:pto},
  required:[rq1,...,rqn]
}

    < 
      (q1@κ(t1) & ... & qk@κ(tk) & 
       ql@κ(ql)? & ... & qm@κ(tm)? &
       u1@κ(sp) & ... & uv@κ(sp) & 
       wc(-[p1,...,pm],+[r1,...,ro])*
      ),
      (wc(r1)@κ(pt1) | wc(-[],-[r1]))*,
      (wc(r2)@κ(pt2) | wc(-[],-[r2]))*,
        ...
      (wc(rn)@κ(pto) | wc(-[],-[ro]))*
    >

where
  l = k+1
  for i<=k, qi=pj and ti=sj and ∃rqh|pj=rqh
  for i>k, qi=pj and ti=sj and ∀rh|pj!=rqh
  for i<=n, ui=rqj where ∀ph|ph!=rqj
  

This looks complicated, but all it is saying is that our mapped content model consists of a mix, in any order, of: properties that are named and required (q1 through qk), properties that are named but not required (ql through qm, properties that are not named but are nevertheless required (u1 through uv), a wildcard to pick up properties that are not named that match none of the patterns but satisfy the schema for additionalProperties, and a wildcard to pick up properties that are not named but do match one of the patterns. The wildcard clauses in the second and subsequent branches of this simultaneous model ensure that properties matching patterns satisfy their appropriate schema: everything matches the pattern and its corresponding schema, or doesn't match the pattern at all. Each pattern gets its own simultaneous branch because an input property may match more than one of them, in which case it would need to satisfy constraints from each match.

If patternProperties is empty, as is often the case, this simplifies a great deal. We can drop the wildcards that match against patterns and simplify the simultaneous model with one branch to just that branch:

{
  properties: {p1:s1,...pm:sm},
  additionalProperties:sp,
  required:[rq1,...,rqn]
}

    (
     q1@κ(t1) & ... & qk@κ(tk) & 
     ql@κ(ql)? & ... & qm@κ(tm)? &
     u1@κ(sp) & ... & uv@κ(sp) & 
     wc(-[p1,...,pm],-[])@κ(sp)*
    )
  

{
  properties: {p1:s1,...pm:sm},
  required:[rq1,...,rqn]
}

  

    (
     q1@κ(t1) & ... & qk@κ(tk) & 
     ql@κ(ql)? & ... & qm@κ(tm)? &
     u1@κ(sp) & ... & uv@κ(sp)
    )
  

Notice that we still get fairly weak content models here: where every property can occur in any order, optional unless specifically required, with all kinds of wildcards unless additionalProperties is explicitly false and there are no patternProperties. This has performance implications, as it creates larger and more complex derivatives. In JSON objects, every property name is unique, however. We can use this knowledge to strengthen the wildcards in the first branch by adding any required properties to the excluded list. (In the examples we will assume we do this.) Other optimizations are possible. We will return to this point later.

Mapping the array-relevant compositional properties follows a similar paradigm, but an additional class of extension is in order, because array members do not have any symbol associated with them, just values. However, given our type constraint scheme, we still have something to say about such things, we just need a little bit more notational mechanism:

Given the type-only expressions, we are now in a position to map array properties. The items property in JSON Schema comes in two varieties with different semantics: as a single schema, or as an array of schemas. If it is a single schema, then that schema applies to every member of the array, and additionalItems is irrelevant. If it is an array, then each member of the array applies one to one to the values in the array in order, with any surplus values in the array matching the additionalItems schema, if any:

  (•@κ(s1),•@κ(s2),...,•@κ(sn),•@κ(sa)*|
   •@κ(s1),•@κ(s2),...,•@κ(sn)?|
   •@κ(s1),•@κ(s2),...,•@κ(sn-1)?|
   ...
   •@κ(s1),•@κ(s2)?|
   •@κ(s1)?
  )

  =

  ((•@κ(s1),
     (•@κ(s2),
        ...
        (•@κ(sn)?,•@κ(sa)*)
        ...
     )?
   )?
  )
  

  (•@κ(s1),•@κ(s2),...,•@κ(sn)?|
   •@κ(s1),•@κ(s2),...,•@κ(sn-1)?|
   ...
   •@κ(s1),•@κ(s2)?|
   •@κ(s1)?
  ) 

  =

  ((•@κ(s1),
    (•@κ(s2),
      ...
      •@κ(sn)?
      ...
    )?
   )?
  )

The reason for the complexity of the rules for items is this: just because the property defines type constraints for three slots, that doesn't mean a matching array must have three entries in it. That is handled by a different constraint property, the minItems property. We could apply it here to remove some of the optionality.

In other words, array constraint properties map to type-only expressions. The additionalItems property is only relevant if the items property enumerates a sequence of type constraints for each item in the array.

Mapping the dependencies property is a little confusing because its value is a JSON object where each value is either a subschema or an array of property names. The semantics are very different, and the dependencies property is likely to bifurcate in future drafts of JSON Schema. Each item in the JSON object maps separately, using a different rule depending on whether its value is a schema or an array.

Here are the rules:

{model: <
     μM({dependencies:{p1:v1}}),
     ...,
     μM({dependencies:{pn:vn}})
   >}

    ((p & wc(-[p],-[])*) ? 
     (q1 & ... & qn & wc(-[q1,...,qn],-[])*) : 
     true)
     

It should also be noted that although at first blush we have made so many extensions to regular expressions that it seems likely that none of the supporting results would hold, in fact we have hardly extended anything substantively. Instead of the finite vocabulary consisting of the symbols in the schema we have a vocabulary consisting of the symbols crossed with the type identifiers plus the • symbol. It is still a finite vocabulary.^[9] The operators and functions we have added, being boolean operators, fit into the rules defined by Brzozowski. True, we have made the rules for matching more complex, but one could also think of them as just being a funny kind of equality. On the other side, while our input can consist of an arbitrary number of distinct values, they are all just annotations on that finite vocabulary. The infinitude of values will concern us when we get to caching, however.

Derivatives

Given a JSON Schema mapped in this way, we can compute derivatives of those expressions with respect to JSON values. Most of these rules come directly from Sperberg-McQueen05 or Brzozowski64 or can be derived by Brzozowski's observation that the derivative of any boolean operator over some operands is the operator over the derivatives of those operands. Algebraically: Δf(R)/Δa = f(ΔR/Δa) for any boolean function f. A key difference is that when we get to the leaves, we have to do type matching as well as just symbol matching. Let us introduce a little more notation:

Taking lowercase a and b as symbols and uppercase E, F, and G as expressions, the derivatives of basic expressions (without type matching) are as follows:

To take the derivative of an expression with respect to a JSON object, first note the edge case for an empty sequence is defined so that:

ΔE/Δε => E
    

ΔE/Δ(u,a) => (ΔE/Δu)/Δa
        

ΔE/Δ(p1,p2,...,pn) => (...(((ΔE/Δp1)/Δp2)/...)/Δpn)
        

Given the set of properties of an object p1, p2, etc., then the derivative of the set of properties is the union of the derivative of each possible sequence starting with some pj:

  (ΔE/Δp1:v1)/Δ•:{p2:v2,p3:v3,...,pn:vn} | 
  (ΔE/Δp2:v2)/Δ•:{p1:v1,p3:v3,...,pn:vn} |
  ... | 
  (ΔE/Δpn:vn)/Δ•:{p1:v1,p2:v2,...,pn-1:vn-1}
        

Adding type matching to the picture doesn't change the rules much although they look a little more complicated. All the rules are the same, just carrying through the type annotation on the expressions, except for the leaf cases where we need to perform a type check as well as a symbol matching:^[10]

  τ({p1:v1,p2:v2,...,pn:vn},λ(T)),
  ((ΔE/Δp1:v1)/Δ•:{p2:v2,p3:v3,...,pn:vn} | 
   (ΔE/Δp2:v2)/Δ•:{p1:v1,p3:v3,...,pn:vn} | 
    ... |
   (ΔE/Δpn:vn)/Δ•:{p1:v1,p2:p2,...,pn-1:vn-1}
  )

Now we have type-aware derivatives for expressions over symbols, we still need to account for arrays and top level values that have no symbols and compute derivatives over these type-only expressions. Arrays unroll like sequences:

What this says is that derivative of an array can be treated mostly as a sequence of non-symbol values, although we need to consider the type constraints on the array as a whole. A symbol cannot match a non-symbol, so derivatives of that kind are empty. A derivative of a non-symbol with respect to a non-symbol value comes down to the type matching function against that value.

Nullability

The nullability function decides whether an expression can be matched against nothing. When the derivative of an expression with respect to the input is not nullable, that means that either it would need additional input in order to match or it has already run down a blind alley and there is no way to match what is there. Therefore the data cannot be valid with respect to that expression. Conversely, when the derivative is nullable, it means that the input has been successfully matched by the regular expression (or consumed by the state machine, if you prefer) and no additional input is necessary for a successful match.

The rules for the nullability function are as follows:

Type Matching

Type matching checks the type constraints of a type T against a particular value v. It returns ε if the value matches the type constraints of the type and ∅ otherwise.

Type-matching evaluates the various facets according to their semantics, something like:

There is an additional rule for the τ function that handles subschemas. This will make more sense after we have looked at some examples:

Given this rule, we can observe that a JSON value is valid with respect to a JSON schema if and only if the type matching function for the mapped JSON schema is ε.

Relations and Simplifications

There are a number of relations and simplifications of the derivative expressions that come in useful in computing derivatives and keeping the size of the derivatives in reasonable bounds.

First, some of the operators are associative:^[11]

(E|(F|G)) = ((E|F)|G) = (E|F|G)
(E,(F,G)) = ((E,F),G) = (E,F,G)
(E&(F&G)) = ((E&F)&G) = (E&F&G)
(F⊕G)⊕H = F⊕(G⊕H) = F⊕G⊕H
<<F,G>,H> = <F,<G,H>> = <F,G,H>
        

Some of the operators are also commutative:

E|F = F|E
E&F = F&E
E⊕F = F⊕E
<E,F> = <F,E>
        

There are straightforward simplifications involving ε, ∅, and redundant expressions. We will make use of these, generally without comment, in the examples.

E|E = E
ε&E = E&ε = E
∅&E = E&∅ = ∅
∅|E = E|∅ = E
ε,E = E,ε = E
∅,E = E,∅ = ∅

E⊕E = ∅
E⊕!E = ε
∅⊕E = E⊕∅ = E

(∅?F:G) = G
(ε?F:G) = F

<E,E> = E
<E,!E> = ∅
<ε,E> = <E,ε> = E
<∅,E> = <E,∅> = ∅
        

These identities mean that, given a function or operator f that can only take the values of ε or ∅, such as the type matching function or the nullability function

<f,E> = f,E
        

Negation behaves as expected with respect to boolean operators:

!(!E) = E
!<E,F> = !E|!F
!(E|F) = <!E,!F>
!(E⊕F) = <!E,!F>|<E,F>
        

Finally, certain of the extension operators can be defined in terms of the others. This can be useful for proving some of these derivations, but it also gives us some comfort that we are not actually enhancing extended regular expressions beyond recognition:

F⊕G = <F|G,!F|!G> 
(F?G:H) = <F,G>|<!F,H>
        

Examples

{ type:"number" }
           

T0: { kind:number, simpleType:"xs:numeric" }
         

τ(47,λ(T0)) = 
  τ(47,{kind:number, simpleType:"xs:numeric"}) = 
  [47 isa number],[47 instanceof xs:numeric] = ε
           

{
  "type": "object",
  "required": ["a","b"],
  "oneOf": [
    {
      "properties": {
        "a": { "type": "number", "minimum": 0 },
        "b": { "type": "number", "minimum": 0 },
        "c": { "type": "number" }
      },
      "additionalProperties": false
    },
    {
      "properties": {
        "a": { "type": "number", "maximum": 0 },
        "b": { "type": "number", "maximum": 0 },
        "d": { "type": "number" }
      },
      "additionalProperties": false
    }
  ]
}
           

T0: {
  kind:object,
  model: 
    <
     (a@T1? & b@T1? & c@T2?) ⊕ (a@T3? & b@T3? & d@T2?),
     (a & b & wc(-[a,b],[])*)
    >
}
T1: {
  kind:number,
  simpleType:"xs:numeric",
  minimumInclusive:0
}
T2: {
  kind:number,
  simpleType:"xs:numeric"
}
T3: {
  kind:number,
  simpleType:"xs:numeric",
  maximumInclusive:0
}
           

{
  a: 1,
  b: -1,
  c: 2
}
           

τ({a:1,b:-1,c:2}, λ(T0)) = 
  τ({a:1,b:-1,c:2}, 
    {
      kind:object,
      model:
        <
          (a@T1? & b@T1? & c@T2?) ⊕
            (a@T3? & b@T3? & d@T2?),
          (a & b & wc()*)
        >
  }) =
  ν(Δ<
    (a@T1? & b@T1? & c@T2?) ⊕ (a@T3? & b@T3? & d@T2?),
    (a & b & wc()*)
    >/Δ•:{a:1,b:-1,c:2}
  )
           

Δ<
  (a@T1? & b@T1? & c@T2?) ⊕ (a@T3? & b@T3? & d@T2?),
  (a & b & wc()*)
>/Δ•:{a:1,b:-1,c:2}
           

(
  Δ<
    (a@T1? & b@T1? & c@T2?) ⊕ (a@T3? & b@T3? & d@T2?), 
    (a & b & wc()*)
  >/Δa:1
)/Δ•:{b:-1,c:2}
           

(
  Δ<
    (a@T1? & b@T1? & c@T2?) ⊕ (a@T3? & b@T3? & d@T2?),
    (a & b & wc()*)
   >/Δa:1
)/Δ•:{b:-1,c:2} =

(
  <
    Δ(
      (a@T1? & b@T1? & c@T2?) ⊕
        (a@T3? & b@T3? & d@T2?)
    )/Δa:1, 
    Δ(a & b & wc()*)/Δa:1
  >
)/Δ•:{b:-1,c:2} =    

(
  <
    Δ(a@T1? & b@T1? & c@T2?)/Δa:1 ⊕ 
      Δ(a@T3? & b@T3? & d@T2?)/Δa:1, 
    Δ(a & b & wc()*)/Δa:1
  >
)/Δ•:{b:-1,c:2} =    
           

Δ(a@T1? & b@T1? & c@T2?)/Δa:1 =
  Δ(a@T1?)/Δa:1 & b@T1? & c@T2? |
  a@T1? & Δ(b@T1?)/Δa:1 & c@T2? |
  a@T1? & b@T1? & Δ(c@T2?)/Δa:1
          

Δ(a@T1?)/Δa:1 = Δa@T1/Δa:1 | ν(a@T1) = 
  [a=a],τ(1,λ(T1)) | ν(a@T1) = 
  τ(1,
    {
      kind:number,
      simpleType:"xs:numeric",
      minimumInclusive:0
    }
   ) = ε
          

        
Δ(a@T1?)/Δa:1 & b@T1? & c@T2? = b@T1? & c@T2?
          

Δ(b@T1?)/Δa:1 = Δb@T1/Δa:1 | ν(b@T1) = ∅ | ∅ = ∅
Δ(c@T2?)/Δa:1 = Δc@T2/Δa:1 | ν(c@T2) = ∅ | ∅ = ∅
          

a@T1? & Δ(b@T1?)/Δa:1 & c@T2? = a@T1? & ∅ & c@T2? = ∅
a@T1? & b@T1? & Δ(c@T2?)/Δa:1 = a@T1? & b@T1? & ∅ = ∅
          

Δ(a@T1? & b@T1? & c@T2?)/Δa:1 = b@T1? & c@T2?
          

Δ(a@T3? & b@T3? & d@T2?)/Δa:1 =
  Δ(a@T3?)/Δa:1 & b@T3? & d@T2?) |
  a@T3? & Δ(b@T3?)/Δa:1 & d@T2? |
  a@T3? & b@T3? & Δ(c@T2?)/Δa:1
          

Δ(a@T3?)/Δa:1 =
  Δa@T3/Δa:1 | ν(a@T3) =
  [a=a],
  τ(1,
    {
      kind:number,
      simpleType:"xs:numeric",
      maximumInclusive:0
    }
  )
          

Δ(b@T3?)/Δa:1 = Δb@T3/Δa:1 | ν(b@T3) = ∅
Δ(d@T2?)/Δa:1 = Δ(d@T2)/Δa:1 | ν(d@T2) = ∅
          

(
  <
    (b@T1? & c@T2?) ⊕ ∅, 
    Δ(a & b & wc()*)/Δa:1
  >
)/Δ•:{b:-1,c:2}
          

Δ(a & b & wc()*)/Δa:1 = 
  (Δa/Δa:1 & b & wc()* |
   a & Δb/Δa:1 & wc()* |
   a & b & Δwc()*/Δa:1) =
  b & wc()*
          

Δwc()*/Δa:1 = Δwc()/Δa:1,wc()* = ∅,wc()* = ∅

<(b@T1? & c@T2?) ⊕ ∅, b & wc()*>/Δ•:{b:-1,c:2} =
  <
   Δ(b@T1? & c@T2?)/Δb:-1 ⊕ Δ∅/Δb:-1, 
   Δ(b & wc()*)/Δb:-1
  >/Δc:2
          

Δ(b@T1? & c@T2?)/Δb:-1 =
  (Δ(b@T1?)/Δb:-1 & c@T2?) | (b@T1? & Δ(c@T2?)/Δb:-1) = 
  ([b=b],τ(-1,λ(T1)) & c@T2?) | (b@T1? & ∅)
          

τ(-1,
  {
    kind:number,
    simpleType:"xs:numeric",
    minimumInclusive:0
  }
) = ∅
          

Δ∅/Δb:-1 = ∅
          

Δ(b@T1? & c@T2?)/Δb:-1 ⊕ Δ∅/Δb:-1 = ∅ ⊕ ∅
          

Δ(b & wc()*)/Δb:-1 = 
  Δb/Δb:-1 & wc()* | b & Δwc()*/Δb:-1 =
  wc()* | b & (Δwc()/Δb:-1,wc()*) =
  wc()* | b & (∅,wc()*) =
  wc()* | b & ∅ = 
  wc()*
          

Δ<∅ ⊕ ∅, wc()*>/Δc:2 = 
  Δ<∅, wc()*>/Δc:2 =
  Δ∅/Δc:2 = 
  ∅
          

[1,"a","b"]
          

{
  type:"array",
  items:[{type:"number"},{type:"string"}],
  additionalItems:false
}
          

T0: {
  kind:array,
  model: •@T1,•@T2
}
T1: {
  kind:number, simpleType:"xs:numeric"
}
T2: {
  kind:string, simpleType:"xs:string"
}
          

τ([1,"a","b"],λ(T0)) =
  τ([1,"a","b"],{kind:array}),τ([1,"a","b"], {model: •@T1,•@T2})
          

Δ(•@T1,•@T2)/Δ•:[1,"a","b"] =
  ((Δ(•@T1,•@T2)/Δ•:1)/Δ•:"a")/Δ•:"b"
          

Δ(•@T1,•@T2)/Δ•:1 = 
  Δ(•@T1)/Δ•:1,•@T2 | ν(•@T1),Δ(•@T2)/Δ•:1 =
  τ(1,λ(T1)),•@T2 =
  τ(1,{kind:number, simpleType:"xs:numeric"}),•@T2 =
  •@T2
          

Δ(•@T2)/Δ•:"a" =
  τ("a",{kind:string, simpleType:"xs:string"}) = ε
         

Δε/Δ•:"b" = ∅
          

{
  type: "object",
  properties: {
    "a": {
       type: "object",
       properties: {
         "b": { type: "integer" }
       },
       additionalProperties: false
     }
  },
  additionalProperties: false
}
          

TO = { kind:object, model: a@T1? }
T1 = { kind:object, model: b@T2? }
T2 = { kind:number, simpleType:"xs:integer" }
          

{
  a: { c: false }
}
          

τ({a:{c:false}}, λ(T0)) = 
  τ({a:{c:false}}, {kind:object}),
  τ({a:{c:false}}, {model: a@T1?})
          

Δ(a@T1?)/Δa:{c:false}
          

Δ(a@T1?)/Δa:{c:false} = 
  Δ(a@T1)/Δa:{c:false} | ν(a@T1) =
  [a=a],τ({c:false},λ(T1)) =
  τ({c:false},λ(T1))
          

τ({c:false},λ(T1)) = 
  τ({c:false},{kind:object}),
  τ({c:false}, {model: b@T2?}) =
  ν(Δ(b@T2?)/Δc:false)
          

Δ(b@T2?)/Δc:false = Δb@T2/Δc:false | ν(b@T2) 
          

τ({c:false},λ(T1)) = ∅
          

Δ(a@T1?)/Δa:{c:false} = ∅
          

Implementation Considerations

The rules given above for mapping object-related properties produce very weak expressions, which require a lot of work to resolve. We could do slightly better if we recall that properties are unique in a JSON object and assume we can always access those properties in a particular order, say, in codepoint order. Then we can use the sequence operator instead of the intermix operator when we don't have wildcards. We could also use the sequence operator and just insert wildcards everywhere, but that is not better than just using intermix. Because JSON property names are unique within a given object, it is easy enough to prune the branches, especially if we recognize the pattern:

Δ(p1@T1? & p2@T2? & .. & pn@TN? & wc()@S*)/Δx:v = 
  (Δp1@T1?/Δx:v & p2@T2? & ... & pn@TN? & wc()@S*) |
  (p1@T1? & Δp2@T2?/Δx:v & ... & pn@TN? & wc()@S*) |
  ...
  (p1@T1? & p2@T2? & ... & Δpn@TN?/Δx:v & wc()@S*) |
  (p1@T1? & p2@T2? & ... & pn@TN? & Δwc()@S*/Δx:v)
        

Furthermore, if x equals any pj we know this can only be nullable if we pick the branch where we take the derivative of that property, because the derivative of any other pi or of the wildcard will be ∅ (the wildcard excludes all property names mapped from properties). That is:

Δ(
  p1@T1? & p2@T2? & ... & pn@Tn? & wc(-[p1,...,pn])@S*
)/Δx:v = 
  ([∃pj|pj=x] ?
   (τ(v,Tj),
     (p1@T1? & ... & pj-1@Tj-1? & pj+1@Tj+1? & ... 
       & pn@Tn? & wc()@S*)
   ) :
   (τ(v,S),
     (p1@T1? & p2@T2? & ... 
       & pn@Tn? & wc(-[p1,...,pn])@S*)
   )
  )
        

Δ(
  p1@T1? & p2@T2? & ... & pn@Tn? & wc([-pi])@S*
)/Δ{q1:v1,q2:v2,...,qm:vm} =
  τ(q1,S1),τ(q2,S2),...,τ(qm,Sm),
  (r1@V1? & r2@V2? & ... & wc(-[p1,...pn])@S*)

where Sj=([∃i|pi=pj]?Ti:S) and 
the rk@Vk are the pi@Si where ∄j|pi=qj
        

It is possible to create yet another extension operator for this case and handle it specially as a performance optimization.

To make this whole scheme worthwhile, we want to amortize the cost of computing derivatives, both within a particular validation episode and across validation episodes. Indeed, the major theme of Brzozowski's paper is that it can be used to construct a finite state automaton for matching the complete extended regular expression. Having constructed such a thing, it can be used again and again. We choose to be slightly more incremental here, and only compute the parts of the machine we actually need, as we go. Experience with this technique in XML Schema has shown that this is more cost effective, as there can be large parts of the state machine that never get accessed by actual data, especially with large schemas.

If we don't worry about type matching, it is pretty straightforward to create a cache of derivative expressions keyed off an expression ID and a symbol.^[13] The expression ID needs to be computed by memoizing it, lest we keep storing the same derivative computation over and over again. That is, from the state machine point of view, we don't want to create lots of redundant states. It is reasonably straightforward to canonicalize expressions for memoization.

It is helpful, in practice, to prune the computed derivatives as much as possible, precomputing any of the predicate functions (such as [a=x] or ν which lead to ε and ∅ values) that can be used to prune further. Here is where the type-matching causes us trouble: we could compute this and prune the derivative, but not if we wish to cache the result, because the cache is keyed only off the symbol, and τ evaluation depends on the value as well.

What is to be done?

There are three basic options:

Not caching means a lot of work calculating answers: we'd probably be better off just using a more direct algorithm and not using derivatives at all. The whole point of this technique was to compute the finite state machine (here implemented in pieces via the cache). Including values in the cache key means that the derivative cache will have a lot of duplicative entries and looks like an unpromising approach, especially when you remember that some of these values are whole JSON objects and arrays. We essentially sacrifice the finiteness of states, as a practical matter. A more promising variation is to cache partial derivatives and add a secondary cache for the unresolved τ calculations. The τ cache only needs to store one bit of information for each type plus value, and we can make different decisions about the sizing and lifespan of entries for the two caches. The partial derivative cache (∂ cache) can be readily shared across validation episodes, while the τ cache could live for only a single episode. We can tune whether the τ cache caches objects and arrays at all, or if so, how large they might be before we don't bother.

Performance

Measure, because it is never what you think

This test performs a simple validation on a small document (~3K) with up to five levels of nesting, a Medline citation, transcribed directly from its XML representation. The JSON Schema imposes structural constraints (required properties, and sub-properties) as well as some value and simple type constraints. The document is repeatedly validated in a single-threaded loop under various regimes. As a baseline, an XML Schema validation of the XML version of the document is also tested (also using derivatives and the same baseline simple type facet testing). The documents are valid against their respective schemas and both documents and schema files are pulled from a pre-warmed cache. The table shows both the validations per second for the first validation, which for some of the regimes is the one that does most of the work, and for subsequent validations.

The variance in these numbers is quite high, although the relative ordering is generally the same.

What is perhaps most interesting here are the negative results:

I believe the answer to the first negative result is that a lot of the work, at least in this schema, is located in the τ checking, not in the property relation constraints, and that the models are simplistic enough that the recursive walk doesn't have to do much beyond looking at the current set of properties, so the work of computing, constructing, and caching derivatives doesn't really pay.

As for the partial derivatives, I think what is going on here is (1) the τ cache is in play regardless, and in this scenario with the same document repeated over and over, it provides a strong benefit and (2) resolving partial derivatives requires construction of more objects representing the resolved derivative, and the top line on performance here is time spent in allocation from the heap. We can see the strong impact of the τ cache by seeing the two orders of magnitude hit to performance when we turn it off. This scenario is clearly a best-case one for the τ cache, as we can see from these numbers.

The strongest performance win here is from simply having compiled schema objects cached, which gives about a 5 times gain for the recursive walk algorithm, and a 20 times gain for the derivative algorithm. The usefulness of the derivative algorithm is much stronger for cached schemas, unsurprisingly, as the work of computing the derivatives can be amortized over multiple validation episodes.

Similar results obtain from running multiple validations in parallel. This test is a validate-on-load one, where 18 thousand Medline citations are loaded into a database after being validated, using 20 threads. Here the performance is overall lower and overall more similar, probably because the update operations dominate performance overall. Here the data is more varied, so the impact of the τ cache is substantially reduced. This test doesn't separate out the costs of the initial use of the schema, and in fact, in effect, each client thread may end up doing some of the initialization work redundantly in parallel, which impacts the amortization.

Again we see the same fundamental negative results: derivatives aren't much better (and here are a little worse, in fact) than a simple recursive walk and derivative caching is not particularly helpful.

This is a somewhat disappointing discovery.

It is entirely possible that there are deficiencies in the specific implementation strategy here. While tying model checking directly to τ simplifies the model of what is going on, I don't think it is a great implementation strategy: you end up computing τ recursively on complex objects over and over as you move through branches of their parent type's derivative. The τ cache helps here somewhat, but it might be better to deal with this as a local validation instead. I believe the numbers from the XML Schema implementation are instructive here because that is how it works: local validity worked from the bottom up. Another approach that might work better is a scheme to cache the fully resolved derivatives also, keyed off the partial derivative expression ID and the actual value of whatever unevaluated τ's it might contain. That would avoid repeated construction of new expression objects whenever we resolve from the ∂ cache.

It is possible to reclaim finiteness and perform full caching by vectorizing the values. Take each distinct facet anywhere in the schema. Each slot in the vector is 1 or 0 depending on whether a particular value satisfies that facet. This then compresses to a binary value of however many bits. While this recovers finiteness, evaluating a lot more facets that necessary in the moment is also not without cost, so it isn't clear what the conditions are where this could be a performance win.

It may well also be the case that the optimization of folding the required property into the mapping for object composition properties is no optimization at all. Perhaps we'd be better served with a mapping like:

μM({
  properties: {p1:s1,...pm:sm},
  patternProperties: {r1:pt1,...,ro:pto},
  required:[rq1,...,rqn]
}) =>
  {model: 
    < rq1 & ... & rqn & wc(-[rq1,...,rqn])*,
      p1@κ(t1)? & ... & pm@κ(sm)? & 
        wc(-[p1,...,pm],+[r1,...,ro])*,
      (wc(r1)@κ(pt1) | wc(-[],-[r1]))*,
      (wc(r2)@κ(pt2) | wc(-[],-[r2]))*,
        ...
      (wc(rn)@κ(pto) | wc(-[],-[ro]))*
    >
  }