olarity Tagger
Type a sentence e.g. Fido runs Load get the cards Build derivation combine to one S Tag read off polarities
New here? Please see this guide before using the app.
apply rule:

Semantic lexicon

The marking-enriched type of each word. Defaults are the author's lexicon; edit any of them. Types are built from base e, t, num and marked arrows (->+, ->-, -> for the dot).

Adapt function

The Adapt function is a list of fix-up lines. When two types do not fit during tagging, the tool tries these lines from top to bottom and uses the first one that matches. If none matches, nothing changes and tagging fails at that spot.

One line looks like this:

RULE : inLeft , inRight => outLeft , outRight :: polLeft , polRight :: LABEL

RULE says where the line may fire: app (application), comp (composition), or coord (coordination).

inLeft , inRight are the two types coming in, and outLeft , outRight are the two types you want instead. The two slots are fixed by role, not by word order: inLeft is the functor (app), the premise that supplies the result codomain (comp), or the left conjunct (coord); inRight is the other one. In a backward rule the functor sits on the right in the sentence but still matches inLeft. In these patterns, an Uppercase letter (like T) stands for any type, and a lowercase letter (like m) stands for any marking. The tool matches the incoming types, then rewrites them to the output.

The last two parts are optional.

polLeft , polRight tell each rewritten side how to pass its polarity down to its child. You can write d (keep the polarity as it is), up, down, eq, flip(...) (turn up into down and back), or md(..., dom) (combine the polarity with a marking taken from the new type; use dom or cod to point at which arrow). If you leave this out, both sides keep their polarity (d , d).

LABEL is just the name shown on the node in the tree. If you leave it out, it shows ADAPT.

What does the H example do?
The verb-lifting rule H. When application meets a verb e -> T and a quantifier argument (e->t) ->m t, it enlarges the verb's argument slot so it can take the quantifier: app : e -> T , (e->t) ->m t => ((e->t) ->m t) ->+ T , (e->t) ->m t. With an empty adapt box you see the raw algorithm, which fails exactly where a fix is needed.
What does the W example do?
The weakening rule W, for coordination. Coordination first lifts any bare individual e to np+ = (e->t) ->+ t on its own (the Montague lift), so the two conjuncts arrive as quantifiers. If their types still differ, W sends both to their join ∨, the least upper bound of the two types in a preorder on types: coord : A , B => Join(A, B) , Join(A, B). For example np+ ∨ np- = np•. For the details, see [Reference].