[TYPES] semantics of `quote'

[Uday Reddy]

Dear Thomas,

The standard approach to dealing with quotation is to think of the
language as operating at two levels: one inside the quotation brackets
and one outside.  An "unquote" operation can take you from the upper
level (quotation level) to the lower level (denotation level).  This
idea can also be generalised to multiple levels.

A search on Google Scholar for "two-level languages" or "multi-stage
languages" will take you to the work of Fleming Nielson, Eugenio Moggi
and others.

Cheers,
Uday

Thomas Streicher writes:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Does anyone know of a reference to work on (denotational) semantics of
> `quote' constructs in functional languages like LISP?
> 
> Probably there is nothing like that since the operational evaluation rule
> 
>      quote M -> "M"   (where "M" is e.g. a Goedel number for M)
> 
> induces an onservational equivalence coinciding with syntactic equality.
> Well, there should be variants if quote is call-by-value where the meaning
> of quote M is a Goedel number of the weak head normal form of M.
> 
> More generally, one might ask for quote constructs  \libqu  where
> \libqu M -> "N" such that M and N have the same denotation (whatever this is).
> 
> The reason why I am asking this on TYPES is that languages with (a kind of)
> quote seem to be necessary for constructing realizabilty models of Martin-Loef
> type theory validating Church's Thesis
> 
>     (\Pi f : N \to N) (\Sigma e : N) (\Pi n:N) {e}(n) = f(n)
> 
> a question brought up recently by M.Maietti and G. Sambin.
> 
> My impression is that a quote construct seems to be incompatible with
> the \xi-rule
>                     M = N
>                  -------------
>                   \x.M = \x.N
> 
> Best regards, Thomas
> 
>