Various questions

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Various questions
Serious Questions

  • For querying, why do we need yet another set of formal definitions at all? As per the slides, we have

    ** deductive queries [m]⊢ F: prop[/m], result is yes/no
    ** concretized queries [m]Γ ⊢ F: prop[/m], result is set of substitutions [m]γ[/m] st. [m]⊢ True[[ F[γ] ]][/m]
    ** computational queries [m]⊢ e[/m], result is [m]⊢ e’[/m] such that [m]⊢ [[e]] ≐ [[e’]][/m]

    These definitions seem very similar to the ones for relative (ded.|concr.|comp.) semantics. For instance, given a translation [m]T: l → L[/m] and a deductive semantics [m]⊢_L[/m] for [m]L[/m], we defined the relative deductive semantics as follows: [m]⊢_l F[/m] iff. [m]⊢_L T(F)[/m]. And this is precisely the notion of what a deductive query is supposed to do.

  • The notes in section 8.1.1 on type systems claim that typing errors in Church-flavored type systems are usually encountered during compile time, and typing errors in Curry-flavored ones usually during runtime. Why is Java, which is Curry-flavored, not a counterexample? The Java compiler typechecks at compile time. Sure, RuntimeExceptions may occur since Java’s type system is unsound, but that’s orthogonal to “Church vs. Curry”, no?

  • see other thread: BOL → SFOL semantics: translation for R* insufficient?

Deeper Questions (I’d judge answers to be probably not relevant for the exam)

Querying: The definitions you cite arise by successive abstraction during the course of the lecture.
If you read it backwards, we have, e.g., |- F: prop with answer yes/no as the primary definition of deductive query/semantics.
Then we specialize to relative semantics and obtain the definitions previously introduced in the lecture.

Typing errors: Any Curry system can do and usually does some type-checking at compile time. But usually it cannot check everything.
For example, in Java, we cannot check statically if a type cast will succeed at run time.

Pullback: The general idea of moving a property forward or backward through a function appears everywhere in math.
A fairly general example is:
relation R: A → B → bool
Property p_A:A → bool and p_B: B → bool.
There are now four basic statements about how p and R interact:
existential preservation: (ex a:A R(a,b) & p_A(a)) => p_B(b)
universal preservation: (fa a:A R(a,b) => p_A(a)) => p_B(b)
existential reflection: (ex b:B R(a,b) & p_B(b)) => p_A(a)
universal reflection: (fa b:B R(a,b) => p_B(b)) => p_A(a)
All 4 statements can be used as potential theorems (if p_A and p_B have already been defined) or as definitions (of p_A in terms of p_B or vice versa).

1 Like