EoPL reading (126) 2.3 Representation Strategies for Data Types

scheme EoPL

待ち時間で整理してみる事に。
まず unify-term の仕様 (というか実装) から。

  • t が var-term の場合
    • u が var-term 又は u に含まれる id に tid が無い場合は unit-subst 手続きに tid と u を渡した結果を戻す
    • 上記の条件に合致しない場合、#f を戻す
  • t が var-term 以外の場合 (constant-term 又は app-term の場合)
    • u が var-term の場合 unify-term に u と t を渡してその戻りを戻す
    • u が constant-term の場合
      • t が app-term なら #f を戻す
      • t が constant-term で、値が同一であれば (empty-subst-rec) を戻す
      • t が constant-term で、値が同一でなければ #f を戻す
    • u が app-term の場合
      • t が constant-term なら #f を戻す
      • t が app-term なら unify-terms に ts と us を渡してその戻りを戻す

ええと、明かに #f が戻るパターンとしては

  • その1
(unify-term '(var-term x) '(app-term ((var-term x))))
  • その2
(unify-term '(constant-term 1) '(app-term ((var-term x))))
  • その3
(unify-term '(constant-term 1) '(constant-term 2))
  • その4
(unify-term '(app-term ((var-term x))) '(constant-term 1))

単純ではないけど、以下もダメかな。

  • その5
(unify-term '(app-term ((var-term x))) '(var-term x))

試験追加してみた。パスしてます。

(test-section "unify-term (2)")
(test* "(unify-term '(var-term x) '(app-term ((var-term x))))"
       #f
       (unify-term '(var-term x) '(app-term ((var-term x)))))
(test* "(unify-term '(constant-term 1) '(app-term ((var-term x))))"
       #f
       (unify-term '(constant-term 1) '(app-term ((var-term x)))))
(test* "(unify-term '(constant-term 1) '(constant-term 2))"
       #f
       (unify-term '(constant-term 1) '(constant-term 2)))
(test* "(unify-term '(app-term ((var-term x))) '(constant-term 1))"
       #f
       (unify-term '(app-term ((var-term x))) '(constant-term 1)))
(test* "(unify-term '(app-term ((var-term x))) '(var-term x))"
       #f
       (unify-term '(app-term ((var-term x))) '(var-term x)))

そろそろ移動します。