What Declarative Languages Are (2013)

https://semantic-domain.blogspot.com/2013/07/what-declarative-languages-are.html

by tel • 6 years ago

36 12 6 years ago

semantic-domain.blogspot.com

What is a trivial existential quantifier and what property identifies them?

empath752• 6 years ago

I’m not sure what a trivial existential quantifier is, but an existential quantifier is the statement ‘there exists’, usually written ∃.

marcosdumay2• 6 years ago

The 'for all' statement is also an existential quantifier, as is the 'this one value' statement implicit on the imperative statements.

The entire meat of the article depends on this concept of "non-trivial" quantifier.

tel2• 6 years ago

I think, loosely, an existential quantifier is "trivial" if you can immediately discharge it. I don't know that there's a very formal approach to this, but there's definitely a way to dream up completely trivial existential quantifiers.

The only obvious one that comes to mind is an existential quantifying over a singular domain. If Unit is the type containing the single value (), then `exists (x: Unit) . P x` is trivially P ().

Even a tiny extension of this (e.g. exists (x: Boolean) . P x) is enough to make this no longer trivial as it at least indicates a search process and can be used to encode arbitrary expansion as long as you can nest existentials.

So that's the other way I could imagine it being trivial: if existentials aren't allowed to index very powerful statements, if the Ps above cannot themselves include quantified statements.

hyperpallium2• 6 years ago

The latex isn't rendering for me. Pasting it into https://math.stackexchange.com/questions/ask is one online solution.

In the example, membership in a language already implies existence, doesn't it? So why is the (crucial) existential quantifier needed?

What does "moded" mean (as in "well-moded")?

empath752• 6 years ago

I do enjoy ‘simple explanations’ that depend on you having a masters degree to understand.

https://www.w3.org/People/Massimo/papers/fpca95.pdf

Explained in that paper. I don’t think I’m qualified to give a tl;dr;

hyperpallium2• 6 years ago

From abstract of an earlier paper co-authored by Reddy

A mode of a predicate designates some of its parameters to be input and the others to be output. ... indefinite modes... in which a resolution interpreter yields answers with free variables. https://www.tib.eu/en/search/id/tema-archive%3ATEMAE84100273...

Sounds like well-moded means: for given inputs, you get a definite answer, rather than something to be further computed around (like high school algebra with more than one unknown). Fits the context here.

tel2• 6 years ago

Existential quantification implies search because, computationally, we want to actually deliver at least one example of the existence.

For instance, the classic puzzle where people sit next to one another at dinner, wearing colored outfits, eating certain dishes, talking about certain topics, all subject to a set of constraints is a search problem. It can be phrased with existentials

    exists (seating in possible_seatings):
      exists (outfits in possible_outfits):
        exists (plating in possible_platings):
          exists (conversation in possible_conversation):
            constraints(seating, outfits, plating, conversation)

This can be seen as an obvious for loop, but for less obvious structures, existential quantification can be powerful. This is especially true when the existentials exist within the language of types that constrain the language of values/computation.

Finally, well-moded is a term from logic programming. It's one condition which allows us to prove that searches like the one above will actually converge either to a refutation of the problem or one or more solutions. In general, using existential quantifiers makes it easy to phrase impossible to solve search programs, so it's important to limit the strength of these languages to sit within, for instance, the well-moded subset.

I won't go over the technical definition of well-moded, but it's basically designed to force a logic program into a simplistic structure for which various smart search algorithms can easily be applied to it.

crazypython• 6 years ago

In particular, note the appearance of an existential quantifier in the premises of the sequential composition and Kleene star cases, and note the nondeterministic choice of a branch in the alternation case. So read as a logic program, this semantics is not well-moded.

Is this saying that you cannot mechanically convert a "declarative language" into a program? Or is it saying it may allow multiple choices? If so, how is it not included in the Curry-Howard correspondence?

What Declarative Languages Are (2013)

Related Stories