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.
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)
Given a translation l → L, a (ded.|concr.|comp.) semantics for L, we can “pullback” a (ded.|concr.|comp.) semantics for l in a natural way, cf. the notes/slides. This reminded me heavily of initial topologies in the field of topology. Can our pullback of semantics for the various aspects be generalized to some categorical notion?
see other thread: Derivation calucli: meta functions vs. substitutions for equality elimination
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).