Logiweb(TM)

7.9.1 Quoting

Prev Up Next Page 212 of 800 Search internet


quote t end quote denotes a data structure which represents the term t. We shall refer to the brackets around t as Gödel brackets, and to quote t end quote as the quoted version of t. We shall refer to the value of a quote as a parse tree.

The quoting construct quote t end quote has many, unusual properties. Among others, it does not respect substitution of equals. As an example, the value of quote 2 + 3 end quote differs from the value of quote 5 end quote even though 2 + 3 = 5. If one asks Logiweb to compute the value of quote 2 + 3 end quote = quote 5 end quote, the value will be false.

Maybe even more surprising, if one asks Logiweb to compute quote 2 + 3 end quote = quote 2 + 3 end quote, then that value will also be false. That is so because quote 2 + 3 end quote does not just denote the term 2 + 3 as such. Each instance of quote 2 + 3 end quote denotes that particular instance of 2 + 3. Each instance contains so-called debugging information which encodes the exact location of the instance on the page. Among others, that debugging information is used when generating meaningful error messages.

One may think of debugging information as a sort of 'radioactive mark' on a term. The mark does not really affect the properties of the term, but it allows to trace a term through processes like macro and tactic expansion.

Prev Up Next Page 212 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05