# How shall I understand the definitions of let expression?

let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus

The simple, non recursive let expression was defined as being syntactic sugar for the lambda abstraction applied to a term. In that definition,

$$( let_s ⁡\quad x = y \quad in \quad⁡ z ) ≡ ( λ x . z ) y$$

let also has another definition in terms of logic, per https://en.wikipedia.org/wiki/Let_expression#Let_definition_in_mathematics says

In mathematics the let expression is described as the conjunction of expressions. In functional languages the let expression is also used to limit scope. In mathematics scope is described by quantifiers. The let expression is a conjunction within an existential quantifier.

$$( ∃ x E ∧ F ) ⟺ let ⁡\quad x : E \quad in \quad⁡ F$$

where $$E$$ and $$F$$ are of type Boolean.

The let expression allows the substitution to be applied to another expression. This substitution may be applied within a restricted scope, to a sub expression.

In the definition $$∃ x E ∧ F$$ by logic,

• Are $$E$$ and $$F$$ both propositions?
• what does $$∃ x E ∧ F$$ mean? Does it mean $$( ∃ x E) ∧ F$$ or $$∃ x (E ∧ F )$$?

• what "substitution" does $$∃ x E ∧ F$$ allow?

• how does $$∃ x E ∧ F$$ relate to the first definition $$( λ x . z ) y$$ ?

Does language C have similar construct to let?

Thanks.

• Existential quantifier has higher precendance than AND operator, so it must mean $(\exists x E) \land F$. I’m not familiar with this “let equivalence”, looks strange – Sandro Lovnički Aug 28 '19 at 5:23
• @SandroLovnički the text says "conjunction within an existential quantifier". I think it can only mean that the conjunction is under the quantifier's scope. Also this is in line with usual notation, when quantifier's scope extends to the right as far as possible. (Also that must be the reason for parenthesis around left-hand side expression.) – Dmitri Urbanowicz Aug 28 '19 at 12:55