Defining a lambda expression to swap the order of lambda abstractions

Question

I want to define a lambda term $\mathrm{swapQ}$ such that

$$\begin{align} \mathrm{swapQ}\ &(\lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \triangleright_\beta\ & (\lambda P Q_1 Q_2. Q_2 (\lambda x_2. Q_1(\lambda x_1. Px_1 x_2))) \end{align}$$

So far I have come up with $$\mathrm{swapQ^*} := \lambda S' P' Q_1' Q_2'. S' P' Q_2' Q_1' \\ \begin{align} \mathrm{swapQ^*}\ &(\lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \triangleright_\beta\ & (\lambda P Q_1 Q_2. Q_2 (\lambda x_1. Q_1(\lambda x_2. Px_1 x_2))) \end{align}$$

but this only swaps the $Q_i$s, not the $\lambda x_i$s that should go with them.

After having fiddled around for a while, I can not seem to find a way to change order of the variable abstractions while leaving the variable occurrences inside the term intact (or vice versa for an equivalent expression). I probably need to abstract over the $(\lambda x_i. \ldots$) parts and reapply them in the same way I did with the $Q$'s, but I can not find the right way to "inject" this override application at the right place without taking the embedded applications with them.

Is what I want to do possible at all? I would appreciate hints for the right technique or perhaps pointers to the literature in case this has been done before.

---

Background:
In Montague grammar for formal natural language semantics, sentences can be formed by consecutively applying $n$ quantified expressions $Q_i$ (where quantified expressions are functions from sets of individuals to truth values) to an $n$-ary verb $P$ (where an $n$-ary verb is a function from $n$ individuals to truth values) to produce a statement. For instance,

$$ \begin{align} & \mathrm{(sentence)(loves)((every)(woman))((a)(man))}\\ \triangleright_\beta & (\mathrm{(every\ woman)}(\lambda x_1. (\mathrm{(a\ man)}(\lambda x_2. \mathrm{loves}x_1x_2))))\\ \triangleright_\beta & \forall x (Wx \to \exists y (My \land Lxy))\\ & \text{"Every woman loves a man"} \end{align} $$ where $$\begin{align} \mathrm{sentence} = & \lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \mathrm{every} = & \lambda P_1 P_2. \forall x (P_1x \to P_2x)\\ \mathrm{a} = & \lambda P_1 P_2. \exists x (P_1x \land P_2x)\\ \mathrm{loves} = & \lambda x y. Lxy\\ \mathrm{woman} = & \lambda x. Wx\\ \mathrm{man} = & \lambda x. Mx\\ \end{align}$$ and application is left-associative ($MNP = (MN)P$).

The purpose of the $\mathrm{swapQ}$ combinator is to swap the two quantified expressions to produce the inverted scope reading, such that

$$\begin{align} & \mathrm{((swapQ)(sentence))(loves)((every)(woman))((a)(man))}\\ \triangleright_\beta & (\mathrm{(a\ man)}(\lambda x_2. (\mathrm{(every\ woman)}(\lambda x_1. \mathrm{loves}x_1x_2))))\\ \triangleright_\beta & \exists y (My \land \forall (Wx \to Lxy))\\ & \text{"There is a man every woman loves"} \end{align}$$ That is, the swapping combinator is applied to the sentence forming combinator such that the order in which the quantified expressions take scope over each other is swapped, while retaining their associated argument position in the verb (determined by which $x_i$ the quantifiers bind to) such that subject remains subject and object remains object.

The motivation is linguistic, but the problem is a purely lambda-technical one, so I figured it is best off at MathSE.

Answer 1

Since $x_1, x_2$ are just dummy variables, one has $$ (\lambda P Q_1 Q_2. Q_2 (\lambda x_2. Q_1(\lambda x_1. Px_1 x_2))) = (\lambda P Q_1 Q_2. Q_2 (\lambda x_1. Q_1(\lambda x_2. Px_2 x_1))) $$

Thus you want $$ \begin{align} \mathrm{swapQ}\ &(\lambda P Q_1 Q_2. Q_1(\lambda x_1. Q_2 (\lambda x_2. Px_1x_2)))\\ \triangleright_\beta\ & (\lambda P Q_1 Q_2. Q_2 (\lambda x_1. Q_1(\lambda x_2. Px_2 x_1))) \end{align} $$ so $\mathrm{swapQ}$ should not only swap $Q_1$ and $Q_2$ but also the order of application on $P$: $$ \mathrm{swapQ} := \lambda S' P' Q_1' Q_2'. S' (\lambda x y.P' y x) Q_2' Q_1' \\ $$

Answer 2

Just out of curiosity, I decided to run this in Combo, which I put up on GitHub. Ok, so first, the lambda expression $$f_0 = λP Q_1 Q_2 · Q_1 (λx_1 · Q_2 (λx_2 · P x_1 x_2))$$ (which is entered in as "$\backslash P\ Q1\ Q2.Q1(\backslash x1.Q2(\backslash x2.P\ x1\ x2))$") reduces to $B (C B) (C B)$, which Combo writes as "$\_0 = C\ B,\ B\ \_0\ \_0$". It reduces to "strong" normal form (as defined and described in the software reference) "$w\ (B\ x\ v)$", when applied to the arguments $v$, $w$ and $x$, thereby leading to the reduction: $$f_0 v w x = w (B x v).$$

The second expression $$f_1 = λP Q_1 Q_2 · Q_2 (λx_2 · Q_1 (λx_1 · P x_1 x_2)),$$ reduces to $B (B T) (B (C B) C)$. When applied to arguments $v$, $w$ and $x$, it reduces to the strong normal form $x (B w (C v))$, thereby leading to the reduction: $$f_1 v w x = x (B w (C v)).$$

The combinators appearing in this are the following lambda expressions $$B = λxyz·x(yz),\quad C = λxyz·xzy,\quad T = λxy·yx.$$

The expression for $f_1$ has the form of a reduction of $f_0$: $$f_1 v w x = x (B w (C v)) = f_0 (C v) x w.$$

Thus, a solution $g$ to $g f_0 = f_1$ can be written as $$g f_0 v w x = f_1 v w x = f_0 (C v) x w,$$ thus $$g = λf_0 v w x · f_0 (C v) x w,$$ which, when entered into Combo (as "$\backslash f0\ v\ w\ x.f0\ (C\ v)\ x\ w$") yields $g = B (B C) (C B C)$.

For comparison, the expression appearing in another reply $$λ S' P' Q_1' Q_2' · S' (λ x y · P' y x) Q_2' Q_1',$$ when entered into Combo (e.g. as "$\backslash Sz\ Pz\ Q1z\ Q2z.Sz\ (\backslash x\ y.Pz\ y\ x)\ Q2z\ Q1z$") also yields $B (B C) (C B C)$. It reduces on four variable as $$g v w x y = v (C w) y x.$$ Thus $$g f_0 v w x = f_0 (C v) x w = f_1 v w x.$$

Under Combo, $g f_0$ will reduce to $f_1$, but requires the η-rule, because it needs three extra dummy variables ($v$, $w$ and $x$) to establish the equivalence. It will reduce $g f_0 v w x$ to $x (B w) (C v)$ and then abstract out the dummy variables to obtain $f_1$. Otherwise, without the η-rule, it will only reduce to $g f_0 = B C (B f_0 C)$, which is a "normal form" (as defined by Combo), but not a "strong normal form".

As another example, take $$ f_0 = λm g h k · g(λx · h(λy · k(λz · m x y z))),\\ f_1 = λm g h k · h(λy · k(λz · g(λx · m x y z))). $$ Under Combo, these yield, respectively $$ f_0 = b (b a),\quad f_1 = c (c (b d)), $$ where $$a = C (B B B),\quad b = B a,\quad c = B (B (C B)),\quad d = B (B C) C.$$ They are each functions that take 4 arguments, given by $$ f_0 w x y z = x (B y (B (B z) w)),\quad f_1 w x y z = y (B z (B (B x) (B C (C w)))). $$ The latter is an instance of the former, with $$f_1 w x y z = f_0 (B C (C w)) y z x.$$ Therefore, a solution to $g f_0 = f_1$ can be given by $$g = λf w x y z·f (B C (C w)) y z x = B (B C) (B (B (B C))) (C B d).$$

When run on $g f_0$ with the η-rule turned on, Combo will produce the expression listed above for $f_1$ as a result.