Displaying similar documents to “Denotational aspects of untyped normalization by evaluation”

Deciding inclusion of set constants over infinite non-strict data structures

Manfred Schmidt-Schauss, David Sabel, Marko Schütz (2007)

RAIRO - Theoretical Informatics and Applications

Similarity:

Various static analyses of functional programming languages that permit infinite data structures make use of set constants like , , and , denoting all terms, all lists not eventually ending in Nil, and all non-terminating programs, respectively. We use a set language that permits union, constructors and recursive definition of set constants with a greatest fixpoint semantics in the set of all, also infinite, computable trees, where all term constructors are non-strict. ...

Multidimensional term indexing for efficient processing of complex queries

Michal Krátký, Tomáš Skopal, Václav Snášel (2004)

Kybernetika

Similarity:

The area of Information Retrieval deals with problems of storage and retrieval within a huge collection of text documents. In IR models, the semantics of a document is usually characterized using a set of terms. A common need to various IR models is an efficient term retrieval provided via a term index. Existing approaches of term indexing, e. g. the inverted list, support efficiently only simple queries asking for a term occurrence. In practice, we would like to exploit some more sophisticated...

Comparing the succinctness of monadic query languages over finite trees

Martin Grohe, Nicole Schweikardt (2004)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

We study the succinctness of monadic second-order logic and a variety of monadic fixed point logics on trees. All these languages are known to have the same expressive power on trees, but some can express the same queries much more succinctly than others. For example, we show that, under some complexity theoretic assumption, monadic second-order logic is non-elementarily more succinct than monadic least fixed point logic, which in turn is non-elementarily more succinct than monadic datalog. Succinctness...

Choice functions and well-orderings over the infinite binary tree

Arnaud Carayol, Christof Löding, Damian Niwinski, Igor Walukiewicz (2010)

Open Mathematics

Similarity:

We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable...