A problem with lambda calculus notation and semantics for function-valued functions

379 Views Asked by At

I would like to understand how to use the $\lambda$-notation to write usual (set-theoretic) functions, and if it is possible at all.

Here are my naïve attempts. Assume that all variables are real-valued. (I am using here the notation with "$\mapsto$" instead of "$\lambda$".)

Example 1.

If $f = x\mapsto \dfrac{1}{x}$ and $g_1 = x\mapsto 2x$, then $g_1\circ f = x\mapsto 2\cdot\dfrac{1}{x}$, and the domain of definition of $g_1\circ f$ is $D_{g_1\circ f}=\mathbf{R}\setminus\{0\}$.

Example 2.

If $h_1 = x\mapsto \left(y\mapsto \dfrac{y}{x}\right)$, then $D_{h_1}=\mathbf{R}$, and $h_1(0)$ is the empty (nowhere defined) function.

Example 3.

If $h_2 = x\mapsto \left(y\mapsto \dfrac{1}{x}\cdot y\right)$, then $h_2 = h_1$ and $D_{h_2}=\mathbf{R}$.

My question.

Consider now $f = x\mapsto \dfrac{1}{x}$ and $g_2 = x\mapsto(y\mapsto xy)$. Then obviously $D_{g_2\circ f} =\mathbf{R}\setminus\{0\}$.

What is the simplest way to write $g_2\circ f$ in $\lambda$-notation (preferably with "$\mapsto$")?

A problem: my naïve attempt to write $g_2\circ f$ gave me, after $\beta$-reduction, the same term as for $h_2$. However, $h_2$ is defined at $0$, but $g_2\circ f$ is not.


Update.

I have realized that a part of this phenomenon does not involve lambda-calculus. The problem is that there is an infinity of ways to "curry" a set-theoretic function of two arguments.

For example, the function $f(x, y) = \dfrac{y}{x}$ of real arguments can be curried as $$ \hat{f}(x) = y\mapsto\frac{y}{x}\colon\mathbf{R}\to\mathbf{R},\quad x\in\mathbf{R}^* =\mathbf{R}\setminus\{0\}, $$ or as $$ \hat{f}(x) = \begin{cases} y\mapsto\dfrac{y}{x}\colon\mathbf{R}\to\mathbf{R} &\text{if}\ x \ne 0\\ \emptyset\ \text{(the empty function)} &\text{if}\ x = 0 \end{cases},\quad x\in\mathbf{R}. $$


Update.

I have stumbled upon virtually my examples in Declarative continuations: an investigation of duality in programming language semantics by Andrzej Filinski (1989):

[...] the uncurried forms of the following two ML functions

fn x=>let t=1/x in (fn y=>t)
fn x=>fn y=>1/x

both compute the inverse of the first argument, but behave differently (the first may fail) in curried form.

1

There are 1 best solutions below

13
On

I don't know whether "I am asking this question here because i am lazy to read through the whole Wikipedia article and to think." is an attempt at honesty or a bad pun. Nevertheless, I think you might benefit from the hint below.

Hint:

The composition operator $\circ$ may be defined as follows (in various notations, pick the one that suits you best):

  • $\operatorname{compose}(f,g)(x) = f (g (x))$,
  • $\operatorname{compose}(f,g) = x \mapsto f (g (x))$,
  • $\operatorname{compose} = (f,g) \mapsto x \mapsto f (g (x))$,
  • $\operatorname{compose} = \lambda (f,g).\ \lambda x.\ f (g\ x)$,
  • $f \circ g \equiv x \mapsto f(g(x))$.

Get to work (and good luck)! :-P