7
$\begingroup$

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?

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

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$.

Lift

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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$. $\endgroup$ – Emil Jeřábek supports Monica Mar 1 at 17:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.