我对可还原表达式(即redex)的理解正确吗? [英] Is my understanding of a reducible expression i.e. redex correct?

问题描述

Hutton在Haskell进行编程说:

Programming in Haskell by Hutton says:

将具有函数形式的表达式应用于一个或多个参数，可以通过执行该应用程序对其进行约简"的过程称为可约简表达式，或简称为redex.

An expression that has the form of a function applied to one or more arguments that can be ‘reduced’ by performing the application is called a reducible expression, or redex for short.

是可还原的表达式，即完全redex

Is a reducible expression i.e. redex exactly

• 一个功能应用程序，其中该功能不是另一个功能应用程序的结果

• a function application where the function is not the result of another function application,

等同于一个函数应用程序，其中函数是函数名还是lambda表达式?

equivalently, a function application where the function is either a function name or a lambda expression?

以上两点之一是我在推荐答案

什么才算是redex取决于语言.表达式的语法是成对引入和消除各种结构的形式. redex是将一种特定类型的构造的引入和消除形式适当地并置的情况.

What counts as a redex generally depends on the language. The syntax of expressions comes in pairs of introduction and elimination forms of various constructs; a redex is when a particular kind of construct's introduction and elimination forms are juxtaposed appropriately.

对于函数，lambdas是介绍(它们是以前没有函数时创建函数的规范方法)，而应用程序是消除(它们是使用函数的规范方法).因此，函数redex是将lambda应用到某些东西，例如形式为(\x -> e1) e2. (而且仅此！将变量应用于某物不是 函数redex.通常我认为这是隐含的，但是您的问题明确询问了这个内容，所以...)

For functions, lambdas are introductions (they are the canonical way to create a function when there wasn't one before) and applications are eliminations (they are the canonical way to use a function). So a function redex is the application of a lambda to something, e.g. something of the form (\x -> e1) e2. (And only this! The application of a variable to something is not a function redex. Normally I would assume this is implied, but your question explicitly asks about this, so...)

对于声明，let-绑定或类似内容是引言(它们是声明名称具有给定值的规范方法)，变量是消除(它们是使用声明值的规范方法).因此，声明redex是let绑定范围内的一个术语，它引用let绑定的变量，例如格式为let x = e1 in e2，其中e2提及x.

For declarations, let-bindings or similar are introductions (they are the canonical way to declare that a name has a given value) and variables are eliminations (they are the canonical way to use a declared value). So a declaration redex is a term in the scope of a let binding that references a let-bound variable, e.g. something of the form let x = e1 in e2 where e2 mentions x.

对于代数数据类型，类型的数据构造函数是引言(它们是在类型中创建值的规范方法)，而case表达式是消除(它们是使用代数类型的值的规范方法).因此，代数数据类型redex是case，其检查对象是完全饱和的构造函数应用程序，例如case Constructor arg1 arg2 arg3 ... of pat1 -> e1; pat2 -> e2; ....

For algebraic data types, the type's data constructors are introductions (they are the canonical way to create a value in the type) and case expressions are eliminations (they are the canonical way to use a value of algebraic type). So an algebraic data type redex is a case whose scrutinee is a fully-saturated constructor application, e.g. case Constructor arg1 arg2 arg3 ... of pat1 -> e1; pat2 -> e2; ....

这些只是配对的一些示例.并非所有语言都具有这三种构造；所有语言都不具有这种构造.还有一些带有其他构造的语言(例如，可变引用，例外等，每种都有自己的介绍和排除形式).但是我认为这应该使您了解"redex"的含义:在这种结构中，可以进行一些计算以逐步找出表达式的值.

These are just some examples of pairings. Not all languages have all three of these constructs; and there are languages with additional constructs (e.g. mutable references, exceptions, and the like, each with their own introduction and elimination forms). But I think this should give you a flavor of what is meant by "redex": it is a construction in which some computation can be done to make forward progress in figuring out the value of an expression.

这篇关于我对可还原表达式(即redex)的理解正确吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！