# what does “lifting” mean?

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?

• I think you're bound for being asked a specific quote or a specific context. – Erwin Smout Oct 30 '12 at 15:36
• In computational geometry, lifting has a very different connotation. I agree with @ErwinSmout that you need to provide more context. – Suresh Venkat Oct 30 '12 at 16:35
• It has yet another meaning in the context of locally testable codes... – arnab Oct 31 '12 at 0:03

Computer science (especially theory B) has many connections to category theory, and that is the usual context for lifting. 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$.

In other words, you will find a morphism $h: X \rightarrow Z$ such that $gh = f$. For more info, see these slides.

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.

There is also 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$$.

• 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 Mar 1 '19 at 17:30