Skip to main content
added 61 characters in body
Source Link
Stéphane Gimenez
  • 1.5k
  • 1
  • 14
  • 29

HereAbout including λ-calculus in the standard complexity model, here is the abstract from some (very) fresh research on the subject. It gives an answer to this question for some restricted form of β-reduction. Basically, complexity in the standard cost model is similar to counting β-reduction steps when restricted to head reduction (which includes call-by-name and call-by-value strategies).

On the Invariance of the Unitary Cost Model for Head Reduction by Beniamino Accattoli and Ugo Dal Lago. (WST2012, link to the proceedings)

The λ-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational diffculty of reducing λ-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the λ-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.

Here is the abstract from some (very) fresh research on the subject. It gives an answer to this question for some restricted form of β-reduction. Basically, complexity in the standard cost model is similar to counting β-reduction steps when restricted to head reduction (which includes call-by-name and call-by-value strategies).

On the Invariance of the Unitary Cost Model for Head Reduction by Beniamino Accattoli and Ugo Dal Lago. (WST2012, link to the proceedings)

The λ-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational diffculty of reducing λ-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the λ-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.

About including λ-calculus in the standard complexity model, here is the abstract from some (very) fresh research on the subject. It gives an answer to this question for some restricted form of β-reduction. Basically, complexity in the standard cost model is similar to counting β-reduction steps when restricted to head reduction (which includes call-by-name and call-by-value strategies).

On the Invariance of the Unitary Cost Model for Head Reduction by Beniamino Accattoli and Ugo Dal Lago. (WST2012, link to the proceedings)

The λ-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational diffculty of reducing λ-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the λ-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.

Source Link
Stéphane Gimenez
  • 1.5k
  • 1
  • 14
  • 29

Here is the abstract from some (very) fresh research on the subject. It gives an answer to this question for some restricted form of β-reduction. Basically, complexity in the standard cost model is similar to counting β-reduction steps when restricted to head reduction (which includes call-by-name and call-by-value strategies).

On the Invariance of the Unitary Cost Model for Head Reduction by Beniamino Accattoli and Ugo Dal Lago. (WST2012, link to the proceedings)

The λ-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational diffculty of reducing λ-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the λ-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.