Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

This is for 

Jira Legacy
serverSystem JIRA
serverId50130123-f232-3df4-bccb-c16e7d83cd3e
keyRHOL-533

...

The algorithm is (men ~ patterns, women ~ terms):

    while ∃ free man m who still has a woman w to propose to {
       w = first woman on m’s list to whom m has not yet proposed
       if w is free
         (m, w) become engaged
       else some pair (m', w) already exists
         if w prefers m to m'
            m' becomes free
           (m, w) become engaged 
         else
           (m', w) remain engaged

This assumes that there are M patterns and N terms and that M = N. 
If M < N, there will not be a match unless there is a wildcard or a remainder (see their sections below) and we should short-circuit unless there is one.

Info
titleDefinition

For the purpose of this document, and general coherence of mental models across the teams, wildcards and remainders should not be counted into the pattern count. They're Their handling is special-case enough to justify this definition by the algorithm simplifications it allows.

...

In such case, the algo above would return an assignment where at least one pattern-term pair is 'married' despite not matching each other. Any such solution means the list of patterns we're matching can't be matched to the list of terms.

We can detect such solutions early, at the end of each iteration of the main loop. At the point where the algo finishes the main loop iteration for a given man m, there's no chance m will get a better option later. In fact, it can only get worse b/c of the swap that happens in lines 6-8. This means, in our case, that once a pattern ends its loop and doesn't have a matching term assigned, we won't be able to match the patterns to the terms and can terminate.

...

Is basically for free. We just run the algorithm for M (#patterns) <= N (#terms) and declare the result a match iff all patterns have a term assigned and there's at least one wildcard in the pattern list. E.g.

Code Block
{ 1 | 2 | 3 } matches { 2 | _ | 1 | _ }

is matching N = 3 terms to a pattern list of M = 2 patterns and K = 2 wildcards, and the match will be successful.

...

The above match will though be successful, as one would expect. This is because, before we reach spatial matching phase, all the match target terms are (and patterns) are fully substituted. In place of each free variable that was defined in the target term's scope, there's now a concrete term.