1

The forward direction is: if $s \equiv_\alpha s' \land t \equiv_\alpha t'$, then $st \equiv_\alpha s't'$. I'm wondering if this holds:

if $st \equiv_\alpha s' t'$ then $s \equiv_\alpha s' \land t \equiv_\alpha t'$.

I was trying to come up with a counterargument, where if for any term $s t$, there exists a way to rewrite it as: $s'' t''$, where $s'' \not \equiv s' \lor t'' \not\equiv t'$, then this property clearly fails. But I haven't found any way to do this, as expanding the terms seem to keep the terms encapsulated inside $s$ or $t$. Maybe I'm missing something.

Thanks!

Kleon
  • 11
  • 2

1 Answers1

1

In an inductive definition of α-equivalence, there is a rule $$\dfrac{s =_α s' \quad t =_α t'}{st =_α s't'}$$ and this is the only way to deduce that two applications are α-equivalent. Hence what you try to (dis)prove is true by definition.

Alternatively, you could have these two rules: $$\dfrac{s =_α s'}{st =_α s't} \qquad \dfrac{t =_α t'}{st =_α st'}$$ then similarly the statement holds.

sparusaurata
  • 438
  • I understand the argument: that rule is the only way to deduce that 2 applications are $\alpha$-equivalent. But, the point that confuses me is that perhaps there exists another way to syntactically rewrite $st$, that is: $st = s''t''$, where $s \not = s'' \lor t \not = t''$. If this method does exist, then we cannot say for a fact that the rule stated will apply for $s$ and $t$. – Kleon Mar 22 '24 at 10:11
  • As pointed out in my answer to your comment under the OP, it depends which rewriting relation we are talking about! But if this is about the α-equivalence relation, then you should (1) consider a formal (inductive) definition of it, (2) prove that the statement holds for the relation you defined. (There exist as many other ways to "syntactically rewrite" terms as you want, but what we care about is α-equivalence and nothing else.) – sparusaurata Mar 22 '24 at 13:02