5

演習 (またはエントリ?) 57 では、ロジックがどのように流れるかを理解していません。問題は、次のことです。

(define teacupo
  (lambda (x)
    (conde
      ((= tea x ) #s)
      ((= cup x ) #s)
      (else #u))))

ここで、'=' は実際には三重棒の統合 (?) 演算子です。以下を実行します。

(run* (r)
  (fresh (x y)
    (conde
      ((teacupo x) (= #t y) #s)
      ((= #f x) (= #t y))
      (else #u)
    (= (cons x (cons y ())) r)))

本は答えを与えます：

((tea #t) (cup #t) (#f #t))

私は答えが次のようになると思っていたでしょう：

(((tea cup) #t) (#f #t))

私の推論は、(teacupo x) の 'x' は、最初にすべてのソリューションを通過し、すべてのソリューションのリストに統合する必要があるということです。しかし、teacupo は一度に 1 つのソリューションしか放棄しないようです。conde の私の解釈では、それが与える規則を使用すると、conde の行を調べて、行が成功した後、失敗したふりをして、変数を更新し、成功する次の行を見つける必要があるため、混乱します。解決策が機能する方法を考えると、そのコードのコンデは成功した行に戻り、茶碗コンデを強制的に失敗させ、次の可能な値をあきらめるように見えます。繰り返しになりますが、teacupo ソリューションはリスト内のすべてのコンデ ソリューションを放棄し、外側のコンデ コールに進むと考えていました。

4

2 に答える 2

4

私の推論は、(teacupo x) の 'x' は、最初にすべてのソリューションを通過し、すべてのソリューションのリストに統合する必要があるということです。

変数xは一度に 1 つの値に統一されます。フォームは、目標を満たす(run* (x) <goals>)値を収集します。x

> (run* (x)
    (teacupo x))
'(tea cup)

の

(conde
  ((teacupo x) (== #t y))
  ((== #f x)   (== #t y)))

成功する方法は 2 つあります。目標(teacupo x)が達成され、そのいずれかxである、teaまたはcup- または - 目標(== #f x)が達成xされて (統合されている)#fである。

要するに、すべての目標を満たす値を一度に 1 つずつ収集しrun*て、可能な値を実行します。xこれはx、一度に 1 つの値に統一されることを意味します。

より簡単な例:

> (run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))
'(1 3)

DrRacket でスニペットを試してみたい方向けの完全なコード:

#lang racket
(require minikanren)
(define-syntax succeed (syntax-id-rules () [_ (fresh (t) (== t t))]))

(run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))    

(define teacupo
  (lambda (x)
    (fresh (result)
      (conde
       ((== 'tea x ) succeed)
       ((== 'cup x ) succeed)))))

(run* (x)
  (teacupo x))

(run* (r)
  (fresh (x y)
    (conde
      ((teacupo x) (== #t y))
      ((== #f x)   (== #t y)))
    (== (cons x (cons y '())) r)))
于 2015-07-05T11:53:57.463 に答える