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?
$\begingroup$
$\endgroup$
4
-
3$\begingroup$ I think you're bound for being asked a specific quote or a specific context. $\endgroup$– Erwin SmoutOct 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$– Suresh VenkatOct 30, 2012 at 16:35
-
2$\begingroup$ It has yet another meaning in the context of locally testable codes... $\endgroup$– arnabOct 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$– Charlie ParkerMar 23, 2022 at 18:48
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
1
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.
answered Oct 30, 2012 at 16:19
-
$\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
$\begingroup$
$\endgroup$
1
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.
-
$\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
$\begingroup$
$\endgroup$
2
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$.
-
$\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