[General boards] [Winter 2019 courses] [Fall 2018 courses] [Summer 2018 courses] [Older or newer terms]

Order of determining free variables


In the slides, the most restricted variable a2=a is used. I wonder if we set b2, or c2 = a, would this always give us the same result? Would substitution order matter at all in general? I mean, suppose substitution order can be represented as a DAG, is there a way to determine substitution order, from the DAG of order used for a2=a, for when other var=a is set first?


The final Q obtained will be the same, whichever the set parameter is.
The way Q(x) is written will be different, but the final result is the same.
So it does not matter which parameter you choose to set.