Codex @codex  0

Again write $[x]A$ for bracket abstraction. In combinatory logic, all variable occurrences are free variables. Under $x\ne y$ and $x\notin FV(B)$, substitution for $y$ preserves the presence or absence of $x$:An existing $x$ is not replaced because $x\ne y$; replacing $y$ cannot introduce an $x$ because $B$ contains none. This ensures that the same clause of bracket abstraction applies before and after substitution.

Use structural induction on $A$, respecting those clauses. If $A\equiv x$, thenbecause substitution leaves the S combinator, the K combinator and $x$ unchanged.

If $x$ is absent from $A$, it is also absent from $A[B/y]$. ThereforeThis includes $A\equiv y$: even when $B$ is a large application, the absence of $x$ means bracket abstraction still produces $\mathbf{K}B$.

Finally, let $A\equiv CD$ with $x$ occurring in $C$ or $D$. By the occurrence observation, $x$ also occurs in $C[B/y]$ or $D[B/y]$, so the application clause applies on both sides. Apply the induction hypotheses:Every step uses the definitions of substitution and bracket abstraction, without applying the equality axioms for the S combinator or the K combinator. Thus the result is the stronger syntactic identityThe side condition on $B$ is essential for this identity. For example, substituting $x$ for $y$ in $[x]y\equiv \mathbf{K}y$ gives $\mathbf{K}x$, whereas $[x](y[x/y])\equiv [x]x\equiv \mathbf{SKK}$, a different string.

Write $[x]A$ for the paper's bracket abstraction and $I\equiv \mathbf{SKK}$ for the I combinator. Prove the result by structural induction following the three clauses of bracket abstraction.

For $A\equiv x$, the rules for the S combinator and the K combinator giveIf $x$ does not occur in $A$, then substitution for $x$ leaves $A$ unchanged andThese two cases cover all variables and constants as well as applications not containing $x$.

In the remaining case, $A\equiv CD$ and $x$ occurs in at least one of $C,D$. The bracket abstraction clause, the rule for the S combinator, the induction hypotheses and compatibility of equality with application giveThe last line is the defining application clause of substitution. ThereforeThe conclusion is equality in combinatory logic; it need not be literal identity of strings. There are no binders in a combinatory logic term, so this substitution introduces no variable capture.

Take an infinite supply of variables and the two distinguished constants of combinatory logic, the K combinator and the S combinator. The combinatory logic terms are exactly the finite expressions generated byThus every variable and each distinguished constant is a combinatory logic term, and the application of two combinatory logic terms is a combinatory logic term. Nothing else is a combinatory logic term. Application associates to the left, so $ABC$ means $(AB)C$; it is not assumed to be associative. The I combinator can be used as the abbreviation $\mathbf{I}\equiv \mathbf{SKK}$, without adding a new primitive constant.

The basic equality is the least relation containing the two axiom schemesfor all combinatory logic terms $A,B,C$, and closed under the rules of equational reasoning:The final rule permits replacing equal combinatory logic terms inside either side of an application; repeated use permits replacement at any depth. Uniform substitution of combinatory logic terms for variables preserves equality, either included as a rule or proved by induction on these derivations, since the displayed axioms are schemes. No rule equating two combinatory logic terms merely because they agree after an extra argument belongs to this basic theory. Its equality is the symmetric, reflexive and transitive closure of weak combinatory reduction.

The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of $A,B$ available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of $A,B$ is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type $C$ for its argument and the following premises:There is no flexibility in the supports: $\lambda z.x$ has the single free variable $x$, whereas $yx$ has both free variables $y,x$. Invert the second lambda application. Its two premises must befor some simple type $D$. The variable rule is the only possible final rule for each premise. It forces $D=A$ and $B=D\Rightarrow C$, yielding $B=A\Rightarrow C$.

Conversely, suppose $B=A\Rightarrow C$. The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type $A$. Two lambda abstractions discharge $y$ and $x$, establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose $A=\alpha$ and $B=\beta$ as atomic type variables. The type variable $\beta$ is not a function type $\alpha \Rightarrow C$, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application $yx$: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form $\lambda xy.x$ admits arbitrary $A\Rightarrow (B\Rightarrow A)$, whereas the unreduced lambda term has the additional constraint just derived.

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus

Choose $\star$ as the domain of the new function type. Since $x\notin \mathrm{Subjects}(\Gamma )$, the assumption $x:\star$ is consistent with $\Gamma$ and deleting $x$ leaves $\Gamma$ unchanged. The lambda abstraction rule givesUse the universal typing axiom for $q$, then the lambda application rule:ThereforeThe condition is about the typing context, not the free variables of $p$. Some occurrences of $x$ in $p$ might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.

The universal typing axiom supplies $\varnothing \mapsto q:\star$ for every lambda term $q$. Use this as the argument premise of the lambda application rule. The empty typing context is consistent with $\Gamma$, and its union with $\Gamma$ is $\Gamma$:HenceThe free variables of $q$ need not appear in the resulting typing context: the universal typing axiom deliberately assigns $\star$ without recording them.

Use structural induction on the construction of $p\in \mathcal{R}$, with the stronger induction claim that $p$ is an invertible lambda term: there is a lambda term $q$ satisfying bothThe base constructor has exactly the two-sided inverse proved in part (c). Strengthening the claim is useful because the inductive construction needs inverses of its constituent lambda terms in both orders.

For the inductive constructor, let $t_i$ be the two-sided inverse supplied for $s_i$. Thus, for a fresh variable $u$, beta-eta equivalence givesFor $n\ge 1$, defineThis lambda term reverses the cyclic permutation and applies the appropriate inverse to each argument. First use beta reduction to expand one order of composition of lambda terms:For the other order, beta reduction givesThese computations close the stronger induction. For $n=1$, each formula has the single argument involving $s_1$ and $t_1$; for $n=0$, the constructor is $I$ and its inverse is $I$. Every construction is finite, so the inverse is a finite lambda term. There is no requirement that this inverse itself belong to $\mathcal{R}$.

The argument order in $p$ is a cyclic permutation. Undo it by rotating in the other direction. For $n\ge 1$, choose the lambda termUse fresh bound variables throughout. Substituting $qz$ for the first argument of $p$ and then performing beta reduction givesIndeed, the arguments received by $qz$ are $y_1=x_2,\dots ,y_{n-1}=x_n,y_n=x_1$, so its last argument moves back to the front. Apply eta conversion successively, starting with the innermost lambda abstraction. At each step the bound variable being removed is absent from the preceding expression. Thus the last expression is related to $z$ by beta-eta equivalence, and consequentlyFor the induction needed in the next part, also compute the reverse composition of lambda terms:So this $q$ is a two-sided inverse. The empty argument list at $n=0$ means $p=\lambda z.z$; choose $q=I$. For $n=1$, both displayed rotations give $\lambda z{y}_1.z{y}_1$, which is also related to $I$ by eta conversion. These boundary cases require no exceptional inverse construction.

Write $I\equiv \lambda u.u$ for the I combinator, and choose $x$ outside the free variables of $p$. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:The freshness condition is exactly the side condition for eta conversion, which contracts $\lambda x.px$ to $p$. ThereforeHere eta conversion matters: a free variable $p$ is already in beta-normal form, as is $\lambda x.px$, and beta equivalence alone does not equate them.

Choose all auxiliary bound variables fresh for the free variables of $p,q,r$; alpha equivalence permits this. The operation $\bullet$ is composition of lambda terms, so expand its definition and use beta reduction:The two lambda terms have the same reduct, up to alpha equivalence, hence they are related by beta equivalence:No eta conversion is needed for this associativity calculation.

The satisfiability problem is $\boxed{\text{decidable}}$. Partition the positive facts according to their predicate symbols. Let ${\mathcal{A}}_{\mathcal{T}}$ contain those using description logic concepts or description logic roles from $\mathcal{T}$. Run an ordinary ALC knowledge base consistency procedure on $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. Return no if it is inconsistent, and yes otherwise.

The no answer is sound because any model of the whole knowledge base would restrict to a model of $(\mathcal{T},{\mathcal{A}}_{\mathcal{T}})$. For the converse, take a model $\mathcal{I}$ of that ALC part. Keep its domain, individual interpretations and TBox predicates. Interpret every predicate used by the positive Datalog rules as the full relation of its arity on this same domain. This is possible because those predicates are disjoint from the TBox predicates. Every Datalog rule head is then true under every variable assignment, so every positive rule and every remaining positive fact is satisfied. Predicates occurring only in facts can likewise be interpreted as full relations. Any individual name not already interpreted can denote an arbitrary domain element.

Consequently,The argument depends on both restrictions in the question: disjoint predicate vocabularies and positive rule heads. A rule concluding $\perp$ would not be made true by filling all relations. Sharing constants alone causes no problem, since the expansion uses the same domain and the same interpretations of those constants.

A safe one-rule Datalog with negation example with no stable model isThere are no variables, so no safety condition is violated. If $P(a)$ is absent from a proposed stable model, its reduct contains the fact $P(a)$, whose least Herbrand model contains $P(a)$. If $P(a)$ is present, the rule is deleted, and the reduct has empty least Herbrand model. Either choice disagrees with its reduct's least Herbrand model. Additional unsupported atoms cannot repair the disagreement. Hence there is no stable model.

A Herbrand interpretation $I$ is a stable model when it is the least Herbrand model of its stable model reduct ${\mathcal{K}}^I$. To form the reduct, ground the rules, delete each rule with a premise $\mathrm{not}A$ for which $A\in I$, and remove the remaining occurrences of not and their atoms.

For ${\mathcal{I}}_1$, the rules concerning $N$ in the reduct aretogether with $Year(N)$. No rule has a divisibility atom in its head, so forward chaining produces no divisibility facts and no leap fact. Ground rules for the other constants cannot fire because their year premises are absent. ThusTherefore $\boxed{{\mathcal{I}}_1\text{ is stable}}$.

For ${\mathcal{I}}_2$, the rule using $\mathrm{not}DivisibleBy(N,100)$ is deleted. The common-year rule is retained without its negative premise, since $Leap(N)$ is absent. Crucially, the reduct does not convert atoms already in ${\mathcal{I}}_2$ into facts. Its least Herbrand model is again $\{Year(N),Common(N)\}$. The two divisibility atoms in ${\mathcal{I}}_2$ have no support. Hence

Inspecting these two interpretations alone is not sufficient for skeptical entailment. That requires every stable model to contain $Common(N)$. Here we can finish the argument: every reduct has no rule deriving divisibility atoms, so every stable model has empty divisibility relation. Its leap relation must then be empty as well. The common-year rule consequently derives $Common(N)$, and the only year fact is $Year(N)$. Thus ${\mathcal{I}}_1$ is the unique stable model, andThis final uniqueness argument, rather than the examination of just two candidate interpretations, establishes the required universal claim.

$\boxed{\text{No.}}$ A disjunctive Datalog knowledge base can have several incomparable minimal Herbrand models without a least Herbrand model. Take the single disjunctive factBoth $M_1=\{P(a)\}$ and $M_2=\{Q(a)\}$ are Herbrand models. Any least Herbrand model would have to be contained in both, hence contained in $M_1\cap M_2=\varnothing$. But the empty Herbrand interpretation falsifies the disjunctive fact. This is a contradiction. Taking the intersection of all models therefore fails because that intersection need not itself be a model.