4
$\begingroup$

While reading a paper Nominal Unification from a Higher-Order Perspective, in the abstract I noticed something feel bit confusing,

Nominal Logic is an extension of first-order logic with equality, name-binding, name-swapping, and freshness of names. Contrarily to higher-order logic, bound variables are treated as atoms, and only free variables are proper unknowns in nominal unification. This allows “variable capture”, breaking a fundamental principle of lambda-calculus.

I know a bit about nominal logic, but as I know it respects $\alpha$-conversion, such as $\lambda x.x \approx_\alpha \lambda y.y$. but I could not understand above statement.

I understand the notion of variable capture which leads to a wrong result during the substitution.

So does variable capture not lead to an incorrect result in nominal logic?

what does it mean saying breaking "variable capture" here?

Can anyone explain with examples?

$\endgroup$
  • 1
    $\begingroup$ We expect references to fulfill the minimal scholarly requirements and be as robust over time as possible. Please take some time to improve your post in this regard. We have collected some advice here. $\endgroup$ – Raphael Nov 15 '16 at 12:42
5
$\begingroup$

Variable capture is the phenomenon which "breaks" things when you do your substitutions in a naive way. For example:

  1. Correct: in the expression $$\int_0^1 (a + x)^2 dx$$ substitute $t^2$ for $a$, to get $$\int_0^1 (t^2 + x)^2 dx.$$

  2. Correct: in the expression $$\int_0^1 (a + t)^2 dt$$ substitute $t^2$ for $a$, to get $$\int_0^1 (t^2 + u)^2 du$$ (we renamed the bound variable $t$ to $u$ on the fly to avoid capturing $t$).

  3. Incorrect: in the expression $$\int_0^1 (a + t)^2 dt$$ substitute $t^2$ for $a$, to get $$\int_0^1 (t^2 + t)^2 dt.$$ (We ended up with a different intergral because $t$ was captured by $dt$).

Similarly, in $\lambda$-calculus:

  1. Correct: $(\lambda x . \lambda y . y x)) y = \lambda z . z y$

  2. Incorrect: $(\lambda x . \lambda y . y x)) y = \lambda y . y y$ (because $y$ was captured).

$\endgroup$
  • $\begingroup$ I updated the question to make it more clear. $\endgroup$ – alim Nov 15 '16 at 15:33
1
$\begingroup$

I find out it. in the higher-order unification, some function is found for variable $X$ such as $ [X \mapsto \lambda y.y ]$, substituting this for $X$ will not lead to variable capture.

in nominal unification, $\lambda a.X \approx \lambda b.b$ yields substitution $[X \mapsto a]$, applying this to original problem yields $\lambda a.a \approx \lambda b.b$ where $a$ is captured.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.