<p>If I remember right, in the denotational semantics of programming languages, lifting is used an a rather abstract roundabout way to express partial correctness:</p>

<p>The so-called "lifting" of a state space $\Sigma$ is its disjoint union with a "bottom" symbol $\bot$, which typically represents a non-terminating or divergent state of computation.  This is written, (again, if I remember right) $\Sigma^\bot=\Sigma\amalg\bot,$ and a (very simple) partial order is imposed on $\Sigma^\bot$ where $\forall \sigma\in\Sigma_\bot, \bot \le \sigma,$ but no two distinct states in $\Sigma$ proper are comparable.</p>

<p>If a "totally correct" denotation of the execution of an arbitrary command in the language is a function
$\mathcal C:\mathcal S\to(\Sigma\to\Sigma),$  and we wish to relax the requirement of termination or convergence, then we have $\mathcal C':\mathcal S\to(\Sigma^\bot\to\Sigma^\bot),$ where $\mathcal C'(\mathcal S)(\bot)=\bot$ and $\forall\sigma\in\Sigma,\mathcal C'(\mathcal S)(\sigma)\le \mathcal C(\mathcal S)(\sigma).$</p>

<p>So $\mathcal C'$ is a partially correct denotation of the semantics of command execution in the language.  This is useful, for example, to express the semantics of a <code>while</code> loop with a <em>loop invariant</em> without regard to whether or not it would actually terminate, while additional machinery, namely a <em>loop variant</em>, would be necessary in order express the termination of a <code>while</code> loop.</p>

CC BY-SA 4.0
2022-03-23T18:47:12.740Z
how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?
Charlie Parker
CC BY-SA 3.0
2012-10-30T19:37:29.923Z
2012-10-30T19:37:29.923Z
justin--
<p>There is also <a href="https://en.wikipedia.org/wiki/Hensel%27s_lemma#Hensel_lifting" rel="nofollow noreferrer">Hensel lifting</a> in modular arithmetic, that allows you to relate roots of a polynomial over a ring of integers modulo prime <span class="math-container">$p$</span> to roots of the same polynomial over integers modulo higher powers of <span class="math-container">$p$</span>, i.e.  <span class="math-container">$p^n$</span> for any integer <span class="math-container">$n&gt;1$</span>.</p>

CC BY-SA 4.0
2019-03-01T17:30:41.533Z
This is just one of many particular instances of the concept explained in Artem Kaznatcheev’s answer. Here, $g\colon Z\to Y$ is the ring homomorphism $\mathbb Z/p^n\mathbb Z\to\mathbb Z/p\mathbb Z$.
Emil Jeřábek
CC BY-SA 4.0
2022-03-23T18:47:16.163Z
how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?
Charlie Parker
CC BY-SA 4.0
2019-03-01T14:52:26.360Z
2019-03-01T14:52:26.360Z
Martin Schwarz
<p>Computer science (especially theory B) has many connections to category theory, and that is the usual context for <a href="http://en.wikipedia.org/wiki/Lift_(mathematics)" rel="noreferrer">lifting</a>. The basic idea is that you might have two objects $X$ and $Y$ that interact in a very intuitive way for you, and so it is easy to define a good morphism $f: X \rightarrow Y$. You might have a more complicated object $Z$ that is easy to relate to $Y$, but it is not obvious how it relates to $X$. So you will look at a morphism $g: Z \rightarrow Y$ and then use category theory to <em>lift</em> $f$ to $Z$ using $g$. </p>

<p><img src="https://i.sstatic.net/4Uo9d.png" alt="Lift"></p>

<p>In other words, you will find a morphism $h: X \rightarrow Z$ such that $gh = f$. For more info, see <a href="http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/ralf.pdf" rel="noreferrer">these slides</a>.</p>

CC BY-SA 4.0
2022-03-23T18:47:07.063Z
how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?
Charlie Parker
CC BY-SA 3.0
2012-10-30T16:19:41.887Z
2012-10-30T16:28:36.557Z
2012-10-30T16:28:36.557Z
Artem Kaznatcheev
<p>I see in certain places "lifting computation" or "lifting" mentioned. I haven't been able to accurately define for myself what is meant by that.</p>

<p>This usually comes up in computer science context. Any ideas what it means?</p>

CC BY-SA 3.0
2012-10-30T15:36:38.347Z
I think you're bound for being asked a specific quote or a specific context.
Erwin Smout
CC BY-SA 3.0
2012-10-30T16:35:44.263Z
In computational geometry, lifting has a very different connotation. I agree with @ErwinSmout that you need to provide more context.
Suresh Venkat
CC BY-SA 3.0
2012-10-31T00:03:38.733Z
It has yet another meaning in the context of [locally testable codes](http://arxiv.org/pdf/1208.5413.pdf)...
arnab
CC BY-SA 4.0
2022-03-23T18:48:59.080Z
how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?
Charlie Parker
<reference-request><terminology>
what does "lifting" mean?
kloop
# what does "lifting" mean?

(Asked by: username_0 on 2012-10-30)

I see in certain places "lifting computation" or "lifting" mentioned. I haven't been able to accurately define for myself what is meant by that.

This usually comes up in computer science context. Any ideas what it means?

**Tags:** reference-request, terminology

> **Comments:**
> **username_1**: I think you're bound for being asked a specific quote or a specific context.  
> **username_2**: In computational geometry, lifting has a very different connotation. I agree with @ErwinSmout that you need to provide more context.  
> **username_3**: It has yet another meaning in the context of [locally testable codes](http://arxiv.org/pdf/1208.5413.pdf)...  
> **username_4**: how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?  

---

## 3 answers

### Answer by username_8 on 2012-10-30. Score: 12 | Accepted answer

Computer science (especially theory B) has many connections to category theory, and that is the usual context for [lifting](http://en.wikipedia.org/wiki/Lift_(mathematics)). The basic idea is that you might have two objects $X$ and $Y$ that interact in a very intuitive way for you, and so it is easy to define a good morphism $f: X \rightarrow Y$. You might have a more complicated object $Z$ that is easy to relate to $Y$, but it is not obvious how it relates to $X$. So you will look at a morphism $g: Z \rightarrow Y$ and then use category theory to *lift* $f$ to $Z$ using $g$.

![Lift](https://i.sstatic.net/4Uo9d.png)

In other words, you will find a morphism $h: X \rightarrow Z$ such that $gh = f$. For more info, see [these slides](http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/ralf.pdf).

> **Comments:**
> **username_4**: how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?  

---

### Answer by username_5 on 2012-10-30. Score: 2

If I remember right, in the denotational semantics of programming languages, lifting is used an a rather abstract roundabout way to express partial correctness:

The so-called "lifting" of a state space $\Sigma$ is its disjoint union with a "bottom" symbol $\bot$, which typically represents a non-terminating or divergent state of computation. This is written, (again, if I remember right) $\Sigma^\bot=\Sigma\amalg\bot,$ and a (very simple) partial order is imposed on $\Sigma^\bot$ where $\forall \sigma\in\Sigma\_\bot, \bot \le \sigma,$ but no two distinct states in $\Sigma$ proper are comparable.

If a "totally correct" denotation of the execution of an arbitrary command in the language is a function
$\mathcal C:\mathcal S\to(\Sigma\to\Sigma),$ and we wish to relax the requirement of termination or convergence, then we have $\mathcal C':\mathcal S\to(\Sigma^\bot\to\Sigma^\bot),$ where $\mathcal C'(\mathcal S)(\bot)=\bot$ and $\forall\sigma\in\Sigma,\mathcal C'(\mathcal S)(\sigma)\le \mathcal C(\mathcal S)(\sigma).$

So $\mathcal C'$ is a partially correct denotation of the semantics of command execution in the language. This is useful, for example, to express the semantics of a `while` loop with a *loop invariant* without regard to whether or not it would actually terminate, while additional machinery, namely a *loop variant*, would be necessary in order express the termination of a `while` loop.

> **Comments:**
> **username_4**: how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?  

---

### Answer by username_6 on 2019-03-01. Score: 1

There is also [Hensel lifting](https://en.wikipedia.org/wiki/Hensel%27s_lemma#Hensel_lifting) in modular arithmetic, that allows you to relate roots of a polynomial over a ring of integers modulo prime $p$ to roots of the same polynomial over integers modulo higher powers of $p$, i.e. $p^n$ for any integer $n>1$.

> **Comments:**
> **username_7**: This is just one of many particular instances of the concept explained in username_8’s answer. Here, $g\colon Z\to Y$ is the ring homomorphism $\mathbb Z/p^n\mathbb Z\to\mathbb Z/p\mathbb Z$.  
> **username_4**: how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation?  

---

