search

ilya-klyuchnikov / sc-mini

SC Mini is a "minimal" positive supercompiler
47 stars 13 forks source link

Fix bug in renaming #11

Closed demarkok closed 5 years ago

demarkok commented 5 years ago

It looks like a bug... If I understand correctly, you want to check that renaming is a bijection, i.e. there are no two entries with different first component and the same second component, and vice versa. If so, look at [(a, d), (c, b), (c, d)]. You're returning Just it, though it's not a bijection.

renaming is pretty messy in general, can I rewrite it?

ilya-klyuchnikov commented 5 years ago

In this case:

gs1 = [[(a, d)], [(c, b), (c, d)]]
gs2 = [[(a, d)], [(c, b)], [(c, d)]]
g gs1 gs2 = Nothing
demarkok commented 5 years ago

oops.. Yep, my fault, this example works fine, sorry.

But [(a, d), (b, e), (c, d)] returns Just it (this time I checked it) So if you intended to check bijectivity, it fails on this counterexample. If you didn't intend to check injectivity, but only functionality of this relation, then you probably don't want to see Nothing on [(a, d), (b, d), (c, e)].

Sorry for bothering in case my claims are irrelevant.

ilya-klyuchnikov commented 5 years ago

In that case a correct substitution is produced: {a -> d, b -> e, c -> d}.

Yep, the term renaming is a bit incorrect/vague here (since it implies bijection), - what is really meant is a substitution which range is variables only.