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?
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.Sign up to join this community
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
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$.