Re: [Brillant-devel] Difference between shallow and deep embedding?

On Tue, 8 Dec 2009 14:47:32 +0100
David MENTRE <[EMAIL PROTECTED]> wrote:

> 2009/12/8 David MENTRE <[EMAIL PROTECTED]>:
> > 2009/12/8 Simão Melo de Sousa <[EMAIL PROTECTED]>:
> >> David,  is your question about what is  deep embedding vs. a
> >> shallow embedding? or the consequence in a COQ formalization of
> >> the B theory?
> 
> While the shallow embedding is relatively clear, I'm not sure to
> really understand what a deep embedding is.
> 
In a nutshell, and for the specific case of B, it is as if even
first-order logic with excluded middle was re-encoded as (yet another)
datatype in Coq.

The consequence is that many theorems have to be re-proved with this
datatype (A & B -> A, etc) but the advantage (described towards the end
of the BiCoq paper I think) is that a lot of proof manipulations can be
automated.

> I am still interested in the consequences of the different kind of
> formalization of B inside Coq.
> 
The subsections about theory (theoretical results, I think) in the
BiCoax paper show some of these dangers.

In a few words, the most prominent danger of a shallow embedding is the
inconsistency of the resulting implementation, even if the consistency
of the original formalism is ensured. For B, the danger is mostly
linked to the use of the choice axiom.

The message is CCed to both of you, but I think it is better to
restrict ourselves to the list if we are all subscribed to it.

-- 
Samuel Colin
E-mail: [EMAIL PROTECTED]
Informations: http://hivernal.org/static/about/


_______________________________________________
Brillant-devel mailing list
[EMAIL PROTECTED]
https://mail.gna.org/listinfo/brillant-devel