1
$\begingroup$

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.

enter image description here

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.


cross: https://www.quora.com/unanswered/What-is-the-definition-of-a-redex-and-what-are-they-for-in-programming-languages-theory

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\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.