Talk:Let expression

Sorry ran out of time to complete this.

My intent is to rearrange existing content out of existing pages that logically belongs together. I am a bit short of references at the moment, which I will attempt to correct. I will try to find time to add references, and go though and correct any problems.

I have re-appropriated an existing page which had a redirect through to Scope (computer science). I think the let expression has more significance in its own right, being the stepping stone through from lambda calculus through to modern functional language.

It is also significant as a construct for a named function, with restricted scope. This is significant because it avoids the problems involved in defining an anonymous function (see Curry's paradox).

I appreciate that the page is still a bit short on background, explanation and references. It also doesn't yet all fit nicely together.

Thepigdog (talk) 15:06, 27 March 2014 (UTC)

Added links in to this page and removed the orphan tags. Finished removing the content that has been moved here to create this page.

Thepigdog (talk) 10:27, 28 March 2014 (UTC)

That little problem has bothered me for a long time.

Thepigdog (talk) 04:06, 29 March 2014 (UTC)

Notes on the problem

The result needed is,

$x\not \in \operatorname {FV} (y)\to (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]$

If we start with,

$(\exists xE\land F)\implies \operatorname {let} x:E\operatorname {in} F$

then,

$\operatorname {let} x:E\operatorname {in} F$

$=\operatorname {let} x:\operatorname {true} =E\operatorname {in} \operatorname {true} \land F$

$=E\land F$

So no point fiddling around with that. May as well start with,

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

and derive,

$x\not \in \operatorname {FV} (y)\to (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]$

The awkward thing is why doesn't this rule apply for Boolean F,

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to (\operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F))$

It applies for all other types, why not Boolean. Why do we need to use,

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))$

for Boolean. And then is there some problem still hiding in the woodwork here.

Its not the only rule that applies only to Boolean,

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

only makes sense if F is Boolean. What I am worried about is the derivation,

$\neg (E\land F)$

$\equiv \neg \operatorname {let} x:E\operatorname {in} F$

$\equiv \operatorname {let} x:E\operatorname {in} \neg F$ ...... if lifting was allowed for Boolean F.

$\equiv E\land \neg F$

which is not true. The second problem that concerns me is if we could somehow counterfeit the Boolean type with another Boolean type that behaved like Boolean but was not Boolean. But then we would not have the rule applying if F was not actually of Boolean type.

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

The argument is the you need both rules to create the contradiction.

$(\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F$

Only applies if F is Boolean, so by not allowing,

$x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to (\operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F))$

when F is Boolean, the contradiction is blocked. So I think it's OK. References ...

Thepigdog (talk) 02:09, 31 March 2014 (UTC)

Narrowing

Narrowing is under construction.

Thepigdog (talk) 04:46, 9 April 2014 (UTC)

Another draft

The notation has changed from (c, v) to (v, l). c was a condition and now l is a set from which a condition is calculated. The order swapped around because it went (c, v) -> (c, v, l) -> (v, l). Anyway it was originally the wrong way round.

Using the list l as data to calculate the condition makes the function application rule less intuitive. I am not really happy about that. But it helps with describing narrowing, and removes the need for other handwaving.

Narrowing is described here within math, when it is really meta programming about math. Its a bit of a shoe horn to make it work in math. And then it is not completely clear how the narrowing is applied in meta programming.

Clear ideas in natural language, translated into math, get twisted around. There is no object identity other than the value that may be used. This is frustrating because the narrowing process is simpler than can be written in math. You don't write math, math writes you.

A lot of checking and examples still needed.

Thepigdog (talk) 19:59, 12 April 2014 (UTC)

Probabilistic value sets

Under construction.

Thepigdog (talk) 12:04, 13 April 2014 (UTC)

Value sets and probabilistic value sets

Moved to a new article Narrowing of algebraic value sets.

It was getting too big and was no longer a good fit with let expressions.

Thepigdog (talk) 12:47, 13 April 2014 (UTC)

Problem with local scope

There is a problem if let expressions are considered to have local scope. It is basically the same problem as with lambda expressions. An expression,

$(2\cdot \operatorname {let} x^{2}=4\operatorname {in} x)=(\operatorname {let} x^{2}=4\operatorname {in} x)+(\operatorname {let} x^{2}=4\operatorname {in} x)$

This is OK if the scope of x is the whole expression. But if x was considered to have a scope local to the let expression, then x could be renamed to y,

$(2\cdot \operatorname {let} x^{2}=4\operatorname {in} x)=(\operatorname {let} x^{2}=4\operatorname {in} x)+(\operatorname {let} y^{2}=4\operatorname {in} y)$

which is no longer true. Not sure how to best deal with this as in common usage in functional languages the let expression is considered to define a function with local scope.

Thepigdog (talk) 03:59, 23 May 2014 (UTC)

Numerous problems with text

As of December 2023 [1], there are numerous problems in this article text. Some glaring ones:

• The text uses $\mathrm {FV} (E)$ to denote the set of free variables in the (lambda-ish) expression $E$ without ever defining or explaining this notation.
• The "mathematical let expression" concept is viewed very much from within the lambda calculus community, as something everybody knows, when outside that community the idea that 'let' is a kind of expression is rather nonstandard. That 'let' appears in numerous phrases for introducing notation is standard, likewise that said notation becomes local to a scope, but that the whole body of that scope (which is often multiple sentences, even paragraphs) should be regarded as just one expression is not; this point of view needs to be introduced.
• The priority rules used for predicate logic are nonstandard. Concretely, $\mathrm {let} \;x:E\;\mathrm {in} \;F$ is presented as equivalent to $(\exists xE\wedge F)$ when it should rather be $\exists x(E\wedge F)$. The catch here is that quantification, having a unary prefix notation, is normally afforded the same priority as negation, in which case $(\exists xE\wedge F)$ denotes the conjunction of $\exists xE$ and $F$, but the whole point of a let is that the $\exists x$ scope spans all of $E\wedge F$.

37.2.252.179 (talk) 07:21, 13 December 2023 (UTC)