search

Drup / dowsing

᚛ A type of divination employed in attempts to locate identifiers matching a given type expression
ISC License
35 stars 4 forks source link

The normal form is not robust. Substitution breaks an invariant of the normal form. #19

Open FardaleM opened 7 months ago

FardaleM commented 7 months ago

Currently, the normal form is not stable by substitution. Tuples are represented as sorted arrays, this property is not preserved by substitution. There are 3 possible ways to fix it:

  1. Change the normal form and remove the constraint on the array to be sorted. This solution has an impact on the equivalence test, which currently relies on this property.
  2. Do the sorting after the substitution. Could have an impact on speed
  3. Use another representation that preserves the equivalence modulo AC.

Also, one need to check that replacing a variable in the head position by an arrow is currently correctly handle.