We need a quotation mechanism that can prevent unification and substitution

[ngeiswei]

Some unification/substitution are currently unpreventable. For instance the following

!(let (quote $x) (quote A) $x)

outputs [A].

In some situations such mechanism is required. One example would when one is reasoning about programs such as (λ $x (f $x) or manipulating quantified statements such as (∀ $x (P $x)). These examples also brings the question of the relationship of such quotation mechanism and the support of a scoping mechanism.

[Necr0x0Der]

I don't get the use case. !(let (quote $x) (quote A) $x) should apparently output A, and !(let (quote $x) (quote (+ 1 1)) $x) should output 2, because you deconstruct quote. If a function manipulates atoms and has Atom type arguments, they will not be reduced. What exactly the case, when these two mechanisms are not enough?

[ngeiswei]

I have real world examples of such quoting/scoping issue. But let me create a short version of such example stripped to the essential, and I'll paste it here.

[Necr0x0Der]

My guess is what you are trying to achieve is something like:

(: proc (-> Atom Atom))
(= (proc (quote $x)) (quote (* $x $x)))
!(proc (quote (+ 1 2)))

But you are concerned specifically with let, so there might be another issue

[ngeiswei]

Here's an example. I could come up with a simpler one but I also want to emphasize the real world use.

The following code attempts to synthesize the function composition operator . by combining AS and AK, corresponding to the S and K combinators of combinatory logic but noted as such to not be confused with S, the successor function.

;; Knowledge base
!(bind! &kb (new-space))

;; K combinator
!(add-atom &kb (: AK (-> $a (-> $b $a))))

;; S combinator
!(add-atom &kb (: AS (-> (-> $a (-> $b $c)) (-> (-> $a $b) (-> $a $c)))))

;; Backward chainer
;; Base case
(= (bc (: $prf $ccln) $_)
   ;; Query the knowledge base for rule or fact
   (match &kb (: $prf $ccln) (: $prf $ccln)))
;; Recursive step
(= (bc (: ($prfabs $prfarg) $ccln) (S $k))
   (let* (;; Recurse on proof abstraction
          ((: $prfabs (-> $prms $ccln)) (bc (: $prfabs (-> $prms $ccln)) $k))
          ;; Recurse on proof argument
          ((: $prfarg $prms) (bc (: $prfarg $prms) $k)))
     (: ($prfabs $prfarg) $ccln)))

;; Find combination of K and S equivalent to function composition.
!(bc (: $prg (-> (-> $b $c) (-> (-> $a $b) (-> $a $c)))) (S (S (S Z)))))

A possible solution is ((AS (AK AS)) AK), which the above code succeeds to synthesize. However, by considering type variables as generic holes it also synthesizes many more combinations that are not equivalent to function composition, but rather specialized forms of it.

One example is AK with type (-> $a $c) (-> (-> $a $a) (-> $a $c))). Which can also be accomplished by calling the backward chainer with maximum depth of 0, as follows

!(bc (: $prg (-> (-> $b $c) (-> (-> $a $b) (-> $a $c)))) Z)

Ideally I would like a way to scope these type variables to express

!(bc (: $prg (∀ $a (∀ $b (∀ $c (-> (-> $b $c) (-> (-> $a $b) (-> $a $c))))))) Z)

in which case AK could not be suggested as a valid solution.

[ngeiswei]

I have similar examples where scoping is on the program side involving λ.