Talk:ΛProlog

Terminology Scoping is not used in λ-Prolog

The terminology scoping is not extremly common in
λ-Prolog, especially not for embedded implication, since
the effect of embedded implication is commulative.

I have changed the programming examples so that
they match figure 3.4 of figure 9.6 Programming in Higher-
Order Logic from Miler and Nadathur.

The reverse example is less commulative, but for
example the proving example adds more and more
hypothesis to natural deduction context.

Jan Burse (talk) Jan Burse (talk) 09:15, 8 November 2024 (UTC)

I believe that the use of "scope" applies well to aspects of lambda Prolog. For example, Figure 5.1 defines the reverse predicate with a lexically scoped auxiliary predicate rev. That example illustrates embedded implications as part of the scoping mechanism. Scope also plays an important role in how abstract datatypes are treated: constructors can be limited to the scope of a module (See, for example, Figure 6.6).

Accumulation doesn't mean that there cannot be scope. For example, the query

?- D1 => ((D2 => G1), G2).

results in a call to G1 with the program D1, D2 and a call to G2 with the program D1. Thus, the clause(s) in D2 are scoped over all proof attempts to prove G1. Dale A Miller (talk) 14:03, 8 November 2024 (UTC)