What Declarative Languages Are (2013) | Hacker News Reader

What Declarative Languages Are (2013)

semantic-domain.blogspot.com

36 pointstel12 comments

> 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?

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")?

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;

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.

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.

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

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

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.

Umm, isnt the universal quantifier by definition not the existential qualifier?

From the comments, it seems likely that the author doesn't have a precise definition of non-trivial. But the framework still feels potentially useful as a way to precisely parameterize disagreements about whether or not a given semantics is declarative.

That said, I'm also having some trouble with the concept. Take for example the rule: there exists x such that succ(x) = y ⊢ dec(y) = x. If we're used to operational semantics which include pattern matching, this feels trivial. But otherwise we have to be clever to avoid exhaustive search.

I'm a bit out of my depth here, but it sort-of feels like 'non-trivial' here means 'I can't immediately/uniquely produce a corresponding well-moded operational semantics'. Whether this lends any clarity might be a matter of taste...

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

If you're making a technical claim, rather than some informal claim whose meaning I'm missing, then "for all" is a universal, not an existential, quantifier. The truth of universal quantification over an empty set is an important part of predicate logic.

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.

Reply on news.ycombinator.com