2
$\begingroup$

In lambda calculus (I will use untyped) if a term containing a redex is beta-reduced to another term, then for some reason they are considered "beta-equal". But the lambda calculus only works one way! Assume that 3 conditions are met:

  1. The original term is finite (for simplicity: it consists of a finite number of characters in de Bruijn notation);
  2. The original term contains at least 1 redex, the number of redexes is unlimited (but finite, which, however, follows from condition 1);
  3. Exactly 1 reduction step can be performed on any redex.

Thus, we get a one-tier tree, where the root is the original term, and the vertices are the terms obtained after the reduction steps over each of the redexes. If I understand correctly, the root term is "beta-equal" to each of the vertex terms.

However, if you try to do the same in the opposite direction, then you should ask the question: for a given (final) term, which ones can be "original"? In other words, which of the (desired) terms can be beta-reduced to a given term?

In this case, obviously, the number of such terms is infinite, since you can take absolutely any term and apply it to a function that erases one of its arguments, while leaving the other as is. But the point is not even that the number of these terms is infinite, but rather that it's pointless to be engaged in finding their complete list; beta reduction is a computational step, not "equality".

In general, it seems to me that the concept of "equality" is rather vague and inapplicable in purely theoretical mathematics and computer science. For example, is 1 + 2 equals 3? In the "algebraic" context - yes, in the "computational" - no, 3 can be obtained both by adding 1 and 2, and, for example, by subtracting 0.141592653589... from pi - options an infinite number, and more than countable. However, even in an "algebraic" context, the relation of equality is too vague and simplistic in most cases.

Moreover, in the lambda calculus, generally speaking, "relationships" like beta reduction belong purely to the metatheory of the lambda calculus, in other words, "inside" the lambda calculus we just reduce, "outside" we think about reduction and talk about the "reduction relation". But there is no "equality" here at all. Why then use this term at all?

Thanks in advance.

$\endgroup$
1
  • 1
    $\begingroup$ Is there a real question here? $\endgroup$ Commented Mar 7, 2023 at 21:53

1 Answer 1

2
$\begingroup$

It seems you are mixing up beta reducibility and beta equality.

Beta contraction (here: from $P_1$ to $P_2$) is a single redex collapsing step:

P1
  >
   P2

Beta reducibility (here: from $P_1$ to $P_5$) is the existence of a series where each step is a beta contraction (collapsing of a redex) or an alpha conversion (renaming of bound variables):

P1               
  >            
   P2 ≡ P3   
          >  
           P4
             >
              P5

Beta equality (here: between $P_1$ and $P_7$) is the existence of a series where each step is a beta contraction forwards, a beta contraction backwards, or an alpha conversion; i.o.w., two terms are beta equal iff there exists a term (here: $P_5$) that both ends of the equality be reduced to:

P1               
  >             
   P2 ≡ P3          P7
          >        <
           P4    P6
             >  <
              P5

So beta equality is by definition not one-directional.

Beta reducibility implies beta equality. It is a special case where the conversion goes strictly in one direction, and the common term that both can be reduced to is the term right of the equivalence sign itself. It is customary to only speak of equivalence even when reducibility holds since that is usually of less interest; perhaps that's what's causing your confusion.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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