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)
-
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).
1 „Gefällt mir“