Comparison between SHAP (Shapley Additive Explanation) and LIME (Local Interpretable Model-Agnostic Explanations) I am reading up about two popular post hoc model interpretability techniques: LIME and SHAP
I am having trouble understanding the key difference in these two techniques. 
To quote Scott Lundberg, the brains behind SHAP:

SHAP values come with the black box local estimation advantages of
  LIME, but also come with theoretical guarantees about consistency and
  local accuracy from game theory (attributes from other methods we
  unified)

I am having some trouble understanding what this 'theoretical guarantees about consistency and local accuracy from game theory' is. Since SHAP was developed after LIME, I assume it fills on some gaps which LIME fails to address. What are those? 
Christoph Molnar's book in a chapter on Shapley Estimation states:

The difference between the prediction and the average prediction is
  fairly distributed among the features values of the instance - the
  shapley efficiency property. This property sets the Shapley value
  apart from other methods like LIME. LIME does not guarantee to
  perfectly distribute the effects. It might make the Shapley value the
  only method to deliver a full explanation

Reading this, I get a sense that SHAP is not a local but a glocal explanation of the data point. I could be wrong here and need some insight into what this above quote means. 
To summarize my ask: LIME produces Local explanations. How are SHAP's explanations different from LIME's? 
 A: *

*LIME creates a surrogate model locally around the unit whose prediction you wish to understand. Thus it is inherently local.


*Shapley values 'decompose' the final prediction into the contribution of each attribute - this is what some mean by 'consistent' (the values add up to the actual prediction of the true model, and this is not something you get with LIME).
But to actually get the shapley values, some decision must be made about what to do/how to handle the values of the attributes 'left out', which is how the values are arrived at. In this decision, there is some choice which could change the interpretation. If I 'leave out' an attribute, do I average all the possibilities? Do choose some 'baseline'?
in a nutshell:
Shapley values actually tell you, in an additive way, how you got your score, but there is some choice about the 'starting point' (i.e. the decision about omitted attributes).
LIME simply tells you, in a local sense, what is the most important attribute around the data point of interest.
