Return to Answer

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here, although I do not know exactly where the fixed point theorem is to be found in this.

Google seems to think that this surname has an acute rather than a hachek.

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here. The result above is on pages 38-9 of Bekic2.pdf in this directory.

Google seems to think that this surname has an acute rather than a hachek.

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here, although I do not know exactly where the fixed point theorem is to be found in this.

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here, although I do not know exactly where the fixed point theorem is to be found in this.

Google seems to think that this surname has an acute rather than a hachek.

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here](http://homepages.cs.ncl.ac.uk/cliff.jones/publications/LNCS177-Bekic/), although I do not know exactly where the fixed point theorem is to be found in this.

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$ with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0)) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0)) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Hans Bekić was a member of the IBM Vienna Laboratory but died in a mountain accident in 1982, leaving a lot of his work unpublished. It was edited and published by Cliff Jones and is available here, although I do not know exactly where the fixed point theorem is to be found in this.