PFPL Chapter 8 Function Definitions and Values

Posted on In Disqus:

This part is not shown on PFPL preview version.

Functions as Language Extensions

A function is defined by binding a name to an abt with a bound variable serves as the argument.

A function is applied by substitute a particular expression of suitable type for a bound variable to get an expression.

First-order functions have domain and range limited to num and str.

Higher-order functions permit arguments and results to be other functions.

First-Order Function

$$
\begin{align}\text{Exp}&&e&&:=&&\text{apply}\lbrace f\rbrace(e)&&f(e)&&\text{application}\\
&&&&&&\text{fun}\lbrace\tau_1;\tau_2\rbrace (x_1.e_2;f.e)&&\text{fun } f(x_1:\tau_1) : \tau_2 = e_2\text{ in }e &&\text{definition}
\end{align}
$$

Expression $\text{fun }f\lbrace \tau_1;\tau_2\rbrace(x_1.e_2;f.e)$ binds function name $f$ within $e$ to pattern $x_1.e_2$ , with argument $x_1$ and definition $e_2$. The domain type is $\tau_1$ and the range type is $\tau_2$.

Judgment $f(\tau_1) : \tau_2$ is called function header of $f$, specifying the domain type and range type of function.

Expression $\text{apply}\lbrace f\rbrace(e)$ instantiates the binding of $f$ with argument $e$.

Statics

Extend the statics in Chapter 4 with the following rules:
$$
\dfrac{\Gamma, x_1 : \tau_1 \vdash e_2 :\tau_2\phantom{“”}\Gamma, f(\tau_1):\tau_2\vdash e:\tau}{\Gamma\vdash \text{fun}\lbrace\tau_1;\tau_2\rbrace (x_1.e_2;f.e):\tau}\\
\dfrac{\Gamma\vdash f(\tau_1):\tau_2\phantom{“”}\Gamma \vdash e :\tau_1}{\Gamma \vdash \text{apply}\lbrace f\rbrace(e) : \tau_2}
$$

Function Substitution

Written $[[x.e/f]]e’​$ with following definition
$$
\dfrac{}{[[x.e/f]]\text{apply}\lbrace f\rbrace(e’)=\text{let}([[x.e/f]]e’;x.e)}
$$

Function name $f$ doesn’t stand for expression and can only occur in an application form $\text{apply}\lbrace f\rbrace(e)$.

Lemma: If $\Gamma, f(\tau_1):\tau_2 \vdash e :\tau$ and $\Gamma, x_1:\tau_1 \vdash e_2:\tau_2$, then $\Gamma \vdash [[x_1.e_2/f]]e:\tau$.

Check Chapter 4 Substitution Lemma, we can do induction on $\Gamma, f(\tau_1) : \tau_2 \vdash e : \tau$.

  • If $x_1.e_2 = \text{plus}(x_1;\text{num}[1919])$ and $e = \text{apply}\lbrace f\rbrace(\text{num[810]})​$, then it follows previous definition and in this way it holds.

Dynamics

$$
\dfrac{}{\text{fun}\lbrace\tau_1;\tau_2\rbrace (x_1.e_2;f.e) \longmapsto [[x_1.e_2/f]]e}
$$

Higher-Order Function

$$
\begin{align}
\text{Typ}&&\tau&&::=&&\text{arr}(\tau_1;\tau_2)&&\tau_1 \to\tau_2&&\text{function}\\
\text{Exp}&&e&&::=&&\text{lam}\lbrace \tau\rbrace(x.e)&&\lambda(x:\tau)e&&\text{abstraction}\\
&&&&&&\text{ap}(e_1;e_2)&&e_1(e_1)&&\text{application}
\end{align}
$$

Statics

$$
\dfrac{\Gamma, x:\tau_1 \vdash e :\tau_2}{\Gamma\vdash \text{lam}\lbrace \tau_1 \rbrace (x.e):\text{arr}(\tau_1;\tau_2)}\\
\dfrac{\Gamma \vdash e_1 :\text{arr}(\tau_2;\tau)\phantom{“”}\Gamma\vdash e_2:\tau_2}{\Gamma\vdash \text{ap}(e_1;e_2):\tau}
$$

Inversion

Suppose $\Gamma \vdash e : \tau$

  1. If $e = \text{lam}\lbrace \tau_1 \rbrace(x.e_2)$, then $\tau =\text{arr}(\tau_1;\tau_2)$ and $\Gamma, x : \tau_1 \vdash e_2 : \tau_2$.
  2. If $e = \text{ap}(e_1;e_2)$, then $\exists \tau_2$ that $\Gamma \vdash e_1 : \text{arr}(\tau_2;\tau)$ and $\Gamma \vdash e_2 : \tau_2$.

Substitution

If $\Gamma, x:\tau \vdash e’:\tau’$ and $\Gamma \vdash e : \tau$, then $\Gamma \vdash [e/x]e’:\tau’$.

Also do induction on $\Gamma, x:\tau\vdash e’:\tau’​$.

Dynamics

Extend dynamics E with the following rules and they are all call-by-value interpretation.
$$
\dfrac{}{\text{lam}\lbrace \tau \rbrace (x.e)\text{ val}}\\
\dfrac{e_1\longmapsto e_1’}{\text{ap}(e_1;e_2) \longmapsto \text{ap}(e_1’;e_2)}\\
\left[\dfrac{e_1 \text{ val} \phantom{“”}e_2\longmapsto e_2’}{\text{ap}(e_1;e_2) \longmapsto \text{ap}(e_1;e_2’)}\right]\\
\dfrac{\left[e_2\text{ val}\right]}{\text{ap}(\text{lam}\lbrace \tau_2\rbrace(x.e_1);e_2) \longmapsto [e_2/x]e_1}
$$

When functions are first class, there is no need for function declarations:

  • Simply replace $\text{fun }f(x_1:\tau_1):\tau_2=e_2 \text{ in }e$ by definition $\text{let }\lambda(x:\tau_1)e_1\text{ be } f \text{ in }e$.
  • Replace second-class function application $f(e)$ by $e_1(e_2)$.

Since $\lambda-$abstractions are values, it makes no difference whether it’s evaluated by-name/value for replacement. But with ordinary definitions, we can give a name to partially applied function like
$$
\text{let }k \text{ be }\lambda(x_1:\text{num})(x_2:\text{num})x_1\\\text{ in let }kz\text{ be }k(0)\text{ in }kz(3)+kz(5)
$$
Without first-class function, we cannot form $k​$.

Preservation

If $e :\tau$ and $e \longmapsto e’$, then $e’:\tau$.

Use call-by-name for the sake of simplicity.
$$
\dfrac{}{\text{ap}(\text{lam}\lbrace \tau_2\rbrace(x.e_1);e_2) \longmapsto [e_2/x]e_1}
$$
Suppose $\text{ap}(\text{lam}\lbrace \tau_2\rbrace(x.e_1);e_2) : \tau_1$, then by inversion lemma $x : \tau_2 \vdash e_1:\tau_1$ and $e_2:\tau_2$. By substitution lemma $[e_2/x]e_1 : \tau_1$. The other rules also follow this kind of proof structure.

Canonical Forms

If $e:\text{arr}(\tau_1;\tau_2)$ and $e \text{ val}$, then $e = \lambda(x_1:\tau_1)e_2$ for some variable $x$ and expression $e_2$ such that $x:\tau_1 \vdash e_2:\tau_2$.

If $e \text{ val}$, then $e$ itself is a lambda abstraction. By inversion lemma it is trivial to get the result.

Progress

If $e : \tau$, then either $e \text{ val}$ or $\exists e’$ such that $e \longmapsto e’$.

Use call-by-name for the sake of simplicity.

  • $e = \text{lam}\lbrace \tau\rbrace (x.e_1)​$, $e \text{ val}​$.
  • $e = \text{ap}(e_1;e_2)​$, then
    • $e_1\longmapsto e_1’$ to get $\text{ap}(e_1;e_2)\longmapsto\text{ap}(e_1’;e_2)$.
    • $e_1 \text{ val}$, then $e_1= \text{lam}\lbrace \tau\rbrace (x.e)$ and $\text{ap}(e_1;e_2)\longmapsto [e_2/x]e$.

Evaluation Dynamics and Definitional Equality

Evaluation Dynamics

$$
\dfrac{}{\text{lam}\lbrace \tau\rbrace(x.e) \Downarrow \text{lam}\lbrace \tau\rbrace(x.e)}\\
\dfrac{e_1\Downarrow \text{lam}\lbrace \tau\rbrace(x.e) \phantom{“”}[e_2/x]e\Downarrow v}{\text{ap}(e_1;e_2) \Downarrow v}
$$

Theorem

$e \Downarrow v \iff e \longmapsto^\ast v​$ and $v \text { val}​$.

  • $\Rightarrow$: Suppose $\text{ap}(e_1;e_2)\Downarrow v$, then by induction we get $e_1\Downarrow \text{lam}\lbrace \tau\rbrace(x.e)$ and $[e_2/x]e\Downarrow v$.

    It is easy to see that if $e_1\Downarrow \text{lam}\lbrace \tau\rbrace (x.e)​$, then $e_1 \longmapsto^\ast \text{lam}\lbrace \tau\rbrace (x.e)​$. Same for $[e_2/x]e \Downarrow v​$.

    Thus we get $\text{ap}(e_1;e_2) \longmapsto^\ast \text{ap}(\text{lam}\lbrace \tau\rbrace (x.e);e_2)\to [e_2/x]e \longmapsto^\ast v$.

  • $\Leftarrow$: Suppose $e \longmapsto^\ast v$, then we can use N-time iteration in Chapter 5 to have induction structure.

    Then by $e \longmapsto e’, e\Downarrow v \Rightarrow e’ \Downarrow v$ in Chapter 7, we can finish the induction.

Definitional Equality

Call-by-name dynamics is defined as
$$
\dfrac{}{\Gamma\vdash \text{ap}(\text{lam}\lbrace \tau\rbrace(x.e_2);e_1)\equiv [e_1/x]e_2:\tau_2}\\
\dfrac{\Gamma \vdash e_1\equiv e_1’:\tau_2 \to\tau\phantom{“”}\Gamma \vdash e_2 \equiv e_2’:\tau_2}{\Gamma \vdash \text{ap}(e_1;e_2)\equiv \text{ap}(e_1’;e_2’):\tau}\\
\dfrac{\Gamma, x:\tau_1\vdash e_2\equiv e_2’:\tau_2}{\Gamma \vdash \text{lam}\lbrace \tau_1\rbrace(x.e_2)\equiv \text{lam}\lbrace \tau_1\rbrace (x.e_2’):\tau_1\to\tau_2}
$$

The call-by-value definitional equality requires that the first rule to have argument be a value.

The call-by-value definition equality judgment takes the form $\Gamma \vdash e_1 \equiv e_2 : \tau$ where $\Gamma$ consists of paired hypotheses $x : \tau, x\text{ val}$.

Dynamic Scope

Previous definition of dynamics of function application is only for expressions without free variables, thus ensuring the result is remain closed. Since substitution of closed expressions can never incur capture, then the scope of variables are not disturbed. The treatment of variables is called static scoping.

The crucial difference is that with dynamic scoping the principle of identification of abt’s up to renaming of bound variable is denied. Thus capture-avoiding substitution is unavailable.

In this way evaluation is only defined for open terms (contrast to closed term), with the binding of free variables provided by an environment mapping variable names to (possibly open) values. The binding of variable is determined as late as possible, at the point where the variable is evaluated, rather than where it bound. If the environment doesn’t provide a binding for a variable, evaluation abort with RTE.

For first-order function, dynamic and static scoping coincide. But in higher-order, two approaches diverge.

For $(\lambda(x:\text{num})x + 7)(42)$, there’s no difference between dynamic/static scoping, outcomes are same.

  • Substitute 42 for $x$ in the body of function before evaluation.
  • The body is evaluated in the presence of the binding of 42.

For higher-order case, consider $e \triangleq (\lambda(x:\text{num}) \lambda (y : \text{num})x +y)(42)$.

  • With static scoping $e$ is evaluated to closed value $v \triangleq \lambda(y:\text{num})42+y$. It makes no difference how the bound variable $x$ is chosen, the outcome will always be the same.

  • With dynamic scoping, $e$ is evaluated to open value $v’ \triangleq \lambda(y:\text{num})x+y$ in which $x$ variable occurs free. When the expression is evaluated, the variable $x$ is bound to 42, but this is irrelevant since the binding is not needed to evaluate the $\lambda-$abstraction.

    The binding of $x$ is not retrieved until such time as $v’$ is applied to an argument, at which point the binding for $x$ in force at that time is retrieved (not the one in force at the point where $e$ is evaluated).

Consider the expression $e’\triangleq (\lambda(f:\text{num}\to\text{num})(\lambda(x:\text{num})f(0))(7))(e)$

  • With evaluated using static scope, the value is 42
  • With evaluated using dynamic scope, the value is 7 (rebind $x$ with 7 before apply $e$ to 0).

Dynamic scope violates the basic principle that variables are given meaning by capture-avoiding substitution.

Dynamic scoping has another problem that type-safety is violated.

Considering $e’\triangleq (\lambda(f:\text{num}\to\text{num})(\lambda(x:\text{str})f(“rua”))(7))(e)$,

Exercise

8.1

Consider an intro of an judgment that
$$
f \Downarrow’x.e \triangleq x \vert \text{apply}\lbrace f\rbrace (x)\Downarrow e
$$
then we can have the environmental evaluation dynamics as
$$
\dfrac{\Delta \vdash [e’/x]e\Downarrow e’’}{\Delta, f \Downarrow’ x.e\vdash \text{apply}\lbrace f\rbrace(e’)\Downarrow e’’}
$$

this is call-by-name evaluation rule.

8.2

The problem is that, how to evaluate the value of lambda abstraction with free variables.

If the evaluation has form like
$$
\dfrac{}{\Delta \vdash \text{lam}\lbrace \tau\rbrace (x.e) \Downarrow \text{lam}\lbrace \tau\rbrace (x.e)}
$$
then it would be the case in substitution-based evaluation dynamics.

One can freeze all the values of all free variables in the $\lambda-$abstraction, then we get the environmental evaluation dynamics as
$$
\dfrac{}{x_1 \Downarrow v_1,\dots,x_n\Downarrow v_n \vdash \text{lam}\lbrace \tau\rbrace(x.e)\Downarrow \text{lam}\lbrace \tau \rbrace (x.[\vec{v}/\vec{x}]e)}
$$

But this method used substitution in the rule, which is a violation of environmental dynamics.

Another variation is to regard $[\vec{v}/\vec{x}]e$ as a form of expression called an closure, at application we have to perform context switch from ambient hypotheses to hypotheses encoded in the closure
$$
\frac{\Gamma\vdash e_1\Downarrow [\vec{v}/\vec{x}]e \phantom{“”}x_1\Downarrow v_1,\dots,x_n\Downarrow v_n\vdash e\Downarrow v}{\Gamma \vdash \text{ap}(e_1;e_2)\Downarrow v}
$$
Both methods suffer from inductive definition abuse (Chapter 3), check the weakening, it doesn’t guarantee addition of new rules in $\Gamma$ will keep the environmental dynamics still holds.