12
$\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$
4
  • 3
    $\begingroup$ I think you're bound for being asked a specific quote or a specific context. $\endgroup$ Oct 30, 2012 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$ Oct 30, 2012 at 16:35
  • 2
    $\begingroup$ It has yet another meaning in the context of locally testable codes... $\endgroup$
    – arnab
    Oct 31, 2012 at 0:03
  • $\begingroup$ how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation? $\endgroup$ Mar 23, 2022 at 18:48

3 Answers 3

12
$\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$
1
  • $\begingroup$ how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation? $\endgroup$ Mar 23, 2022 at 18:47
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$ how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation? $\endgroup$ Mar 23, 2022 at 18:47
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$
2
  • $\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$ Mar 1, 2019 at 17:30
  • $\begingroup$ how would you explain this to a mere programmer (that doesn't know category theory, maths etc.)? What is an intuitive/conceptual explanation? $\endgroup$ Mar 23, 2022 at 18:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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