Talk:Lambda lifting

What's the language used in the code examples? SML, maybe? I think it should be noted in the text. Electrolite 00:58, 16 January 2006 (UTC)

Agree
I totally agree. I am a haskell beginner and got more then one problem to solve. I tried to compile the first code fragment with GHC and failed because of "in sum 100". Please add which language is used !

Rewriting rules

What do the rewriting rules have to do with anything? The procedure given for lambda lifting looks complete; but then the example includes an extra phase that involves converting the program to rewrite rules. Furthermore the rewrite process seems to be demonstrating the evaluation strategy of a lazy language like Haskell, rather than a strict one like OCaml. In the interests of simplicity and consistency, I think the rewrite rules should be removed. Ezrakilty 10:58, 4 July 2007 (UTC)

I second that.HenkeB (talk) 22:32, 27 September 2008 (UTC)

Corrections to the code

While the current code does demonstrate the algorithm, it would be clearer and closer to the meaning of the text if the functions sum and f (after lifting) were made into global functions. In both of the current cases, the entire length of code is contained in a single expression. It's clearer and more common in practice to see it written more like this:

(I don't know O'caml too well, so ignore any minor syntax errors). before:

fun sum n = let f x = n + x in
            if equal n 1
               then 1
               else f (sum (n - 1)) 
sum 100

and after:

fun f x w = w + x
fun sum n = 
            if equal n 1
               then 1
               else f (sum (n - 1)) n
sum 100

Tac-Tics 14:34, 16 September 2007 (UTC)

Lambda Lifting in Lambda calculus

I have added this section describe the lambda lifting process as applied to a lambda expression. Its a bit technical, but I hope to make it more readable.

@inproceedings{Johnsson85,
  added-at = {2009-05-10T18:36:57.000+0200},
  address = {Mancy},
  author = {Johnsson, Thomas},
  biburl = {http://www.bibsonomy.org/bibtex/212be202f5c808edcc95a13cfcadd9f25/dparigot},
  booktitle = {Conf. on Func. Prog. Languages and Computer Architecture.},
  description = {Attribute Grammar},
  interhash = {99ea4c776c16996227f481fabd7f597a},
  intrahash = {12be202f5c808edcc95a13cfcadd9f25},
  keywords = {imported},
  publisher = {ACM Press},
  timestamp = {2009-05-10T18:36:57.000+0200},
  title = {Lambda Lifting: Transforming Programs to Recursive Equations},
  url = {http://www.cs.chalmers.se/\~johnsson/Papers/lambda-lifting.ps.gz},
  year = 1985
}

Thepigdog (talk) 13:10, 16 July 2013 (UTC)

Lambda lifting section needs revision

This section needs revision! In particular, you should stop talking eta-reduction and eta-expansion.

In both lambda-lifting and lambda-dropping, no eta-conversion is involved. --- Plmday 14:17, Oct 19, 2013 — Preceding unsigned comment added by Plmday (talk • contribs) 12:21, 19 October 2013 (UTC)

An eta-redex is ,

$\operatorname {eta-redex} [\lambda x.(f\ x)]=f$

If you assume that the eta-redex of an expression equals the expression, this can be rearranged as,

$f\ x=y\iff f=\lambda x.y$

This is used in the example 3.4,

$p\ f=\lambda x.f\ (x\ x)$

is converted to,

$p\ f\ x=f\ (x\ x)$

I think the example is fairly easy to follow. Clearly we are lifting the expression $\lambda x.f\ (x\ x)$ and the resulting lift requires the eta conversion to put it in a function only (no lambda form). As described above at the start of section 3, we are discussing how lambda lifting can demonstrate the equivalence of any lambda expression to an equivalent lambda abstraction free form. The conversion is necessary for this, and I consider it as part of the lift.

Thepigdog (talk) 07:25, 22 October 2013 (UTC)

I have restructured the section Rules for Lambda lifting to make each step simpler. I hope it more clearly explains the lifting process, and the role of eta reductions.

Thepigdog (talk) 03:38, 25 October 2013 (UTC)

Needs further explanation

I have seen the tag,

"However it does not demonstrate the soundness of Lambda calculus for deduction, as the eta reduction[further explanation needed] used in Lambda lifting is the step that introduces cardinality problems into the Lambda calculus, because it removes the value from the variable, without first checking that there is only one value that satisfies the conditions on the variable (see Curry's paradox)."

I agree it needs explanation. Some summary level explanation is provided in Curry's paradox#No_resolution_in_Lambda_Calculus. However I think a new page is needed discussing this issue, based on Curry's papers, called Deductive lambda calculus. I will attempt to create a page for this soon and link this line to it.

Regards Thepigdog (talk) 15:36, 17 February 2014 (UTC)

I have written an article Deductive lambda calculus and provided a link to it. Does this explanation satisfy you?

Thepigdog (talk) 01:16, 22 February 2014 (UTC)

Let expression page created

Content was taken for translation between let and lambda and put in the Let expression article. But now this article does not follow a smooth progression. Lifting and dropping was mixed with translation between lambda and let. How to simplify this article and make it accessible?

• Lambda lifting/dropping in let expressions only
• Lambda lifting/dropping in let+lambda
• Lambda lifting/dropping as conversion between lambda calculus and let expressions (existing).

Need a simple and accessible start, if later it is complex.

Thepigdog (talk) 14:24, 4 April 2014 (UTC)t

Problem with the link to Closure Conversion

It redirects to this page, so it does not make sense.

Vlad Patryshev (talk) 15:02, 23 February 2017 (UTC)

Closure conversion listed at Redirects for discussion

An editor has asked for a discussion to address the redirect Closure conversion. Please participate in the redirect discussion if you wish to do so. Nowak Kowalski (talk) 21:32, 19 April 2019 (UTC)

Subproof to Lemma conversion in Fitch Derivations

Has anyone published remarks along the following lines: converting a conditional introduction (i.e. subproof) in a Fitch derivation to a stand alone lemma shares the syntactic transformations of lambda lifting? 70.171.155.43 (talk) 23:21, 19 December 2020 (UTC)