# What is the definition of a redex and what are they for in programming languages literature?

I saw the word "redex" in the context of proramming language theory/semantics in 2018 and now when I was reading a neurosymbolic research paper (machine learning with neural nets + symbolic algorithms).

The research paper said:

Constructing $$I\beta'$$ (operator that inverts one step of beta-reductions/function applications) depends on careful consideration of the reduction operator we aim to invert (see [39] and Appen- dix F). The operator $$I\beta'$$ builds both top-level redexes and also recurses to build redexes within the body of an expression

The 2018 course says:

In an RSEC language definition one starts by defining the syntax of evaluation contexts, or simply just contexts, which is typically done by means of a context-free grammar (CFG). A context is a program or a fragment of program with a hole, where the hole, which is written $$\Box$$ , is a placeholder for where the next computational step can take place. If $$c$$ is an evaluation context and $$e$$ is some well-formed appropriate fragment (expression, statement, etc.), then $$c[e]$$ is the program or fragment obtained by replacing the hole of $$c$$ by $$e$$. Reduction semantics with evaluation contexts relies on a tacitly assumed (but rather advanced) parsing mechanism that takes a program or a fragment $$p$$ and decomposes it into a context $$c$$ and a subprogram or fragment $$e$$, called a redex, such that $$p = c[e]$$. This decomposition process is called splitting (of $$p$$ into $$c$$ and $$e$$). The inverse process, composing a redex $$e$$ and a context $$c$$ into a program or fragment $$p$$, is called plugging (of $$e$$ into $$c$$). These splitting/plugging operations are depicted in Figure 3.28.

So is a redex just a fragment of a program? Is that all? Curious why this needs a term of its own. It's use and importance.

A redex is an expressions on which we can perform a computation step, such as:

1. fst (a, b) is a redex, it computes to a
2. snd (a, b) is a redex, it computes to b
3. (λ x . x + x) 6 is a redex, it computes to 6 + 6
4. if true then A else B is a redex, it computes to A

Here are some examples which are not redexes: fst p, if x < 6 then 3 else 4, 42, λ x . x + x.

An expression may contain a redex, for instance in

λ x . if x < 6 then fst (4, 5) else x


there is a redex, namely fst (4, 5). In general, an expression may contain main redexes. Which ones are evaluated and in what order depends on how the language is designed.