天天看點

邏輯程式設計入門--clojure.core.logic

此文已由作者張佃鵬授權網易雲社群釋出。

歡迎通路網易雲社群,了解更多網易技術産品營運經驗。

1. 邏輯程式設計思維:

邏輯程式設計(邏輯程式設計)是種程式設計範型,它設定答案須比對的規則來解決問題,而非設定步驟來解決問題。過程是:

事實+規則=結果

簡單的說,事實就是一些已知輸入,規則是應該遵循的限定條件,輸入和輸出應該遵循一定的規則,然後找出所有滿足這些規則的輸出,便是結果。在邏輯程式設計時,我們沒必要去關心尋找結果的過程,而注重的是輸出結果。   邏輯程式設計的要點是将正規的邏輯風格帶入計算機程式設計之中,數學家和哲學家發現邏輯是有效的理論分析工具,很多問題可以自然地表示成一個理論。說需要解答一個問題,通常與解答一個新的假設是否跟現在的理論無沖突等價。邏輯提供了一個證明問題是真還是假的方法。建立證明的方法是人所皆知的,故邏輯是解答問題的可靠方法。邏輯程式設計系統則自動化了這個程式,人工智能在邏輯程式設計的發展中發揮了重要的影響。

2. clojure.core.logic概述:

  clojure.core.logic是clojure一個庫,專門為了實作邏輯程式設計,core.logic是miniKanren的一個實作。miniKanren中一個重要的概念就是goal,根據goal來推測可能的結果,這就是它的核心概念。   我們在使用core.logic程式設計時,擷取邏輯程式設計的結果,一般都遵循以x下形式:

   (run* [logic-variable]
       logic-expressions)
   ;;or
   (run n [logic-variable]
       logic-expressions)      

  run或者run函數可以執行邏輯表達式,傳回滿足條件的結果。傳回的結果是一個關于logic-variable的數組。如果是run則傳回所有滿足邏輯表達式條件的邏輯變量,如果是run n,則傳回前n個滿足條件的變量。這裡要注意的一點是:普通的邏輯表達式的傳回結果隻有兩種:succeed/fail,如果找到滿足條件的結果,則傳回succeed,否則傳回fail。隻有使用run函數才能傳回最終我們想要的輸出結果。下面是run函數的使用示例:

;;首先要導入clojure.core.logic庫
(use 'clojure.core.logic)

;;使用run*,會傳回所有滿足條件的結果
(run* [q]
     ;;這裡是邏輯表達式,後面會講到
     (conde
       [(== q 1)]
       [(== q 2)]
       [(== q 3)]
       ))
;;=>(1 2 3)

;;傳回前兩個結果
(run 2 [q]
     (conde
       [(== q 1)]
       [(== q 2)]
       [(== q 3)]
       ))
;;=> (1 2)

;;如果n大于所有滿足條件結果的總數,則與run*傳回結果一緻
(run 4 [q]
     (conde
       [(== q 1)]
       [(== q 2)]
       [(== q 3)]
       ))
;;=> (1 2 3)      

  當然run函數也可以接收多個參數,如果是多個參數,則以數組的形式傳回:

;;接收兩個參數,最後傳回結果是一個包含數組的序列
(run* [q1 q2]
      (== q1 1)
      (== q2 1)
      )
;;=> ([1 1])      

3. 邏輯表達式以及常用函數:

  邏輯表達式的傳回結果都是succeed或者fail,一個邏輯表達式中可以繼續嵌套另外一個邏輯表達式,下面在介紹clojure中的常用邏輯函數同時穿插的介紹如何使用邏輯程式設計:

(1)==/!=/membero函數:

  "=="/"!="函數用于判斷兩個邏輯變量是否相等或者不相等,是最常用的邏輯函數,而(membero  x  l)函數則表示隻有x屬于數組l時才會傳回succeed:

;;找出等于1的數字
(run* [q] (== q 1))
;;=> (1)

;;找出不等于1且屬于數組[1 2 3]中的數字
;;;;這裡的(!= q 1)與(membero q [1 2 3])兩個邏輯表達式是與的關系(也就是必須兩個邏輯表達式同時滿足才傳回succeed)
(run* [q] 
     (!= q 1)
     ;;q隻有是數組[1 2 3]中的一個元素,才會傳回succeed
     (membero q [1 2 3]))
;;=> (2 3)      
(2)fresh函數:

  這個函數在邏輯程式設計時特别重要,如果我們想在邏輯表達式中用到其他變量怎麼辦?怎麼像其它語言一樣去聲明一個局部變量??fresh函數正是來解決以上疑問的,fresh函數可以聲明幾個局部的邏輯變量,有了這些局部邏輯變量以後,您就可以在邏輯表達式中随意發揮了:

;;q是一個包含兩個元素的數組,第一個元素等于1,第二個元素是[2 3 4]中的一個
;;fresh函數和run函數使用規則類似,都接收一個[參數],參數後面是并列的表示與關系的邏輯表達式
(run* [q]
      (fresh [q1 q2]
             (== q1 1)
             (membero q2 [2 3 4])
             (== q [q1 q2])
             ))
=> ([1 2] [1 3] [1 4])      
(3)succeed/fail

  這兩個邏輯表達式也比較常用,succeed就表示執行成功的邏輯表達式,fail就表示執行失敗的邏輯表達式,下面我們定義一個邏輯表達式函數,輸入參數是一個邏輯表達式,然後傳回該輸入參數的相反的結果:

;;該函數傳回參數g的相反結果:
(defn l-not [g]
  (conda
    (g fail)
    (succeed)
    ))
;;=> #'insight.main/l-not;;在run*函數中使用l-not函數
(run* [q]
      (l-not (== 3 1))
      (== q 1)
      )
;;=> (1)      
(4)conde/conda/condu函數/all函數:

  在介紹fresh函數和run函數時提到這兩個函數的主體部分的表達式是“與”的關系,那麼怎麼可以表達“或”的關系呢,conde/conda/condu這三個函數都可表示“或”的關系,但三者之間又有細微的差别,都是很實用的函數。   這裡之是以要把all函數和它們三個函數放在一起,是因為在conda和condu函數中,會經常使用all函數。

  -->conde函數:接收邏輯表達式組,隻要滿足其中任意一個表達式組,多個表達式組之間是or的關系,不像其他語言中的or函數,conde函數不存在求值短路現象,會傳回分别滿足所有表達式組的結果:

;;傳回滿足等于1,或者同時等于2和3,或者是字元串"yes"/"no"的結果
(run* [q]
      (conde
      ;;其中[]表示的是一組表達式,[]中邏輯表達式預設是“與”的關系,這裡[]也可以用()替換,但是為了差別,最好用[]
        [(== q 1)]
        [(== q 2) (== q 3)]
        [(membero q ["yes" "no"])]
        ))
;;=> (1 "yes" "no")      

  -->conda函數:該函數傳回第一個滿足條件的表達式組中的所有結果,但是特别要注意的是,相鄰兩個表達式組之間切換的條件,也就是如果第n個表達式組傳回fail的情況下,什麼情況下去繼續求解第n+1個表達式組,假設第n個表達式組中有3個表達式[expr1  expr2  expr3],隻有當expr1失敗的情況下,才會執行第n+1個表達式組,否則即使expr1傳回succeed,expr2傳回fail,conda函數就會直接傳回fail,不會執行第n+1個表達式組。   那麼如果我們想要使隻要expr1、expr2,expr3有一個不成立就會執行第n+1個表達式組,怎麼辦??使用all函數,把這三個表達式包含進去。這裡邏輯有點混亂,看代碼會清楚很多:

;;情況1:conda函數中,第一個表達式組中兩個表達式都傳回succeed,是以直接傳回(2 3),不去執行第二個表達式組
(run* [q]
      (conda
        ;;表達式組1:
        [succeed
         (conde
           [(== q 2)]
           [(== q 3)]
           )]
         ;;表達式組2:
        [(membero q ["yes" "no"])]
        ))
;;=> (2 3)

;;情況2:第一個表達式組中第一個表達式傳回fail,則會繼續執行第二個表達式組,是以傳回("yes" "no")
(run* [q]
      (conda
      ;;表達式組1:
        [fail
        ;;表達式嵌套
         (conde
           [(== q 2)]
           [(== q 3)]
           )]
      ;;表達式組2:
        [(membero q ["yes" "no"])]
        ))
;;=> ("yes" "no")

;;情況3:第一個表達式組中第一個表達式傳回succeed,但是整個表達式傳回fail,則不會執行第二個表達式,直接傳回fail
(run* [q]
      (conda
        [succeed
         fail
         (conde
           [(== q 2)]
           [(== q 3)])
         ]
        [(membero q ["yes" "no"])]
        ))
;;=> ()

;;情況4:可以用all函數改變情況3的執行結果
(run* [q]
      (conda
        [(all
           succeed
           fail
           (conde
             [(== q 2)]
             [(== q 3)]))
         ]
        [(membero q ["yes" "no"])]
        ))
=> ("yes" "no")      

  -->condu函數:condu函數是conda函數的子集,它隻傳回conda函數傳回結果集中的結果:

;;情況1:傳回結果是conda傳回結果的第一個元素
(run* [q]
      (condu
        ;;表達式組1:
        [succeed
         (conde
           [(== q 2)]
           [(== q 3)]
           )]
         ;;表達式組2:
        [(membero q ["yes" "no"])]
        ))
;;=> (2)

;;情況2:傳回結果是conda傳回結果的第一個元素
(run* [q]
      (condu
      ;;表達式組1:
        [fail
         (conde
           [(== q 2)]
           [(== q 3)]
           )]
      ;;表達式組2:
        [(membero q ["yes" "no"])]
        ))
;;=> ("yes")

;;情況3:傳回結果是conda傳回結果的第一個元素
(run* [q]
      (condu
        [succeed
         fail
         (conde
           [(== q 2)]
           [(== q 3)])
         ]
        [(membero q ["yes" "no"])]
        ))
;;=> ()      
當然以上所有邏輯表達式都可以嵌套使用。      
(5)matche/matcha/matchu函數:

  這三個函數的第一個參數是一個元素,該元素用于比對後面的表達式組中第一個元素,類似于其它語言中的case函數,如果比對成功,則執行該表達式組中的其它表達式。該三個函數與conde/conda/condu相對應:matche傳回使任意一個表達式組成立的所有元素,matcha隻傳回所有表達式組中第一個使條件成立的所有元素,而matchu傳回所有表達式組中第一個使條件成立的第一個元素:   -->matche函數:

;;用p去比對每個表達式組中的第一個元素(這裡的第一個不能是表達式,隻能是元素),比對成功則會執行後面的表達式,有沒有很像case的趕腳,抛去第一個元素以後的比對規則與conde一模一樣:
(run* [q]
      (fresh [p]
             (matche [p]
                     (['virgin] succeed fail)
                     (['olive]  (conde
                                  [(== q 1)]
                                  [(== q 2)]
                                  ))
                     (['oil] (== q 3)))
             ))
;;=> (3 1 2)      

  -->matcha函數:

;;這裡的matcha函數還是有一點與conda函數不一樣的地方,matcha不會關心每個表達式組中第一個表達式是否比對成功,就像加了all一樣:
(run* [q]
      (fresh [p]
             (matcha [p]
                     ;;這裡雖然第一個表達式成功,但是還是會比對後面的表達式組
                     (['virgin] succeed fail)
                     (['olive]  (conde
                                  [(== q 1)]
                                  [(== q 2)]
                                  ))
                     (['oil] (== q 3)))
             ))
;;=> (1 2)      

  -->matchu函數:

;;matchu則是傳回所有可能比對的第一個元素,執行規則與matcha類似:
(run* [q]
      (fresh [p]
             (matchu [p]
                     ;;這裡雖然第一個表達式成功,但是還是會比對後面的表達式組
                     (['virgin] succeed fail)
                     (['olive]  (conde
                                  [(== q 1)]
                                  [(== q 2)]
                                  ))
                     (['oil] (== q 3)))
             ))
;;=> (1)      
(6)defne/defna/defnu函數:

  這三個函數都是用來定義一個比較特殊的logic函數,這三個函數分别與matche/matcha/matchu三個函數的pattern相比對,它們的比對規則如下:

;;用defn定義含有matche的函數:
(defn fun1 [val]
    (match [val]
        ([val1] expr11 expr12)
        ([val2] expr21 expr22)
    ))
;;fun1函數與下面的fun2函數等價:
(defne fun2 [val]
    ([val1] expr11 expr12)
    ([val2] expr21 expr22)
)      

  下面是這三個函數的使用示例:

;;defne函數:
(defne exampleo [a b]
       ([:a y] (membero y [:x :y]))
       ([:b x] (membero x [:x :y :z])))
;;=> #'insight.main/exampleo(run* [q]
      (fresh [a b]
             (== q [a b])
             (exampleo a b)
             ))
;;=> ([:a :x] [:b :x] [:a :y] [:b :y] [:b :z])

;;defna函數:
(defna exampleo [a b]
       ([:a y] (membero y [:x :y]))
       ([:b x] (membero x [:x :y :z])))
;;=> #'insight.main/exampleo(run* [q]
      (fresh [a b]
             (== q [a b])
             (exampleo a b)
             ))
;;=> ([:a :x] [:a :y])

;;defnu函數:(defnu exampleo [a b]
       ([:a y] (membero y [:x :y]))
       ([:b x] (membero x [:x :y :z])))
;;=> #'insight.main/exampleo(run* [q]
      (fresh [a b]
             (== q [a b])
             (exampleo a b)
             ))
;;=> ([:a :x])      
(7)組合類函數:appendo/conjo/conso/featurec函數

  -->conjo/conso/appendo: conjo函數/conso函數與clojure.core中的conj函數/cons函數相似,隻不過conj/cons傳回組合後的結果,而conjo/conso是将組合後的結果當作參數傳入,判斷三個參數能否組合成功,這兩個函數都是元素與數組的組合,而appendo函數則是數組與數組的組合,判斷兩個數組連接配接是否可以組成第三數組:

;;conjo函數判斷将第二個參數加到第一個參數數組的末尾是否等于第三個參數
(run* [q]
      (conjo q 5 [1 2 3 4 5])
      )
;;=> ([1 2 3 4])

;;conso函數判斷将第一個參數加到第二個參數數組的首部,是否等于第三個參數
(run* [q]
      (conso 1 q [1 2 3 4 5])
      )
;;=> ((2 3 4 5))

;;appendo函數判斷前兩個數組連接配接是否哦等于第三個數組
(run* [q]
      (appendo [1 2] q [1 2 3 4 5])
      )
=> ((3 4 5))      

  至于為什麼上述兩個傳回結果一個是vector,一個是list,這與conj/cons函數的形式一緻,可能往首部插時轉換為連結清單形式,而尾部則是數組(我猜的)   -->membero函數/featurec函數:   membero/featurec函數主要是判斷元素的存在性,membero函數某個元素是否屬于某個數組,而featurec函數則用于判斷某個map是否為另一個map的子集:

;;判斷第二個map是否為第一個map的子集,這裡特别要注意,map中的key一定是要給定的,隻能value是未知數
(run* [q]
      (fresh [q1 q2]
             (featurec {:a 1 :b 2 :c 3} {:a q1 :b q2})
             (== q [q1 q2])
             ))
;;=> ([1 2])

;;membero函數:
(run* [q]
      (membero q [1 2 3 4 5])
      )
=> (1 2 3 4 5)      
(8)and/or函數

  and和or是另一個版本的的all和conde,它們的差別是:   ->and和or:  隻接收一個清單作為參數,清單裡的多個表達式之間的關系是“與”/“或”,   ->all函數: 接收多個表達式作為參數,多個表達式之間的關系是“與”,   ->conde函數: 接收多個表達式清單作為參數,多個表達式清單之間的關系是“或”

;;四個函數輸入參數的差別:
(and* [a b c])
(or* [a b c])
(all a b c)
(conde [a] [b] [c])      

  下面我們用五重點内容種不同的形式表達:q屬于[1 2 3]和[2 3 4]的交集或者q=5

;;or*/and*:
(run* [q]
      (or* [
            (and* [(membero q [1 2 3])
                   (membero q [2 3 4])])
            (== q 5)])
      )
;;=> (5 2 3)

;;or*/all:
(run* [q]
      (or* [
            (all (membero q [1 2 3])
                 (membero q [2 3 4]))
            (== q 5)])
      )
;;=> (5 2 3)

;;conde/all:
(run* [q]
      (conde [(all (membero q [1 2 3])
                 (membero q [2 3 4]))]
             [(== q 5)])
      )
;;=> (5 2 3)

;;conde/and*:
(run* [q]
      (conde [
            (and* [(membero q [1 2 3])
                   (membero q [2 3 4])])]
             [(== q 5)])
      )
;;=> (5 2 3)

;;conde的每個表達式組中的表達式之間預設情況下是“與”的關系
(run* [q]
      (conde [
              (membero q [1 2 3])
              (membero q [2 3 4])]
             [(== q 5)])
      )
;;=> (5 2 3)      
(9)clojure普通函數在logic代碼中的使用:

  通過前面的叙述我們知道,邏輯表達式的傳回結果隻有兩種情況:succeed/fail,如果我們想在clojure.core.logic中調用let、mapv、reduce等clojure普通函數怎麼辦??我們是不是需要将這些函數的傳回結果轉換為succeed或者fail。其實這些事情core.logic中已經為我們做好了,它提供了一個project宏專門為我們解決logic代碼中調用普通函數的問題:

;;因為邏輯變量a/b/c都要被普通函數調用,是以在project的第一個參數清單中将其聲明,然後我們就可以在let中調用其他普通函數,最後将結果傳回便可,傳回的結果一定也是一個邏輯表達式結果
(run* [q]
      (fresh [a b c] 
             (membero a [[1 7] [2 10]])
             (== b [3 8])
             (== c [5 6])
             (project [a b c]
                      (let [result (concat a b c)
                            result-sum (apply + result)
                            result-avg (/ result-sum (count result))]
                        (== q result-avg)))
             ))
;;輸出結果是兩個組數組的平均值
;;=> (5 17/3)      

免費體驗雲安全(易盾)内容安全、驗證碼等服務

更多網易技術、産品、營運經驗分享請點選。

相關文章:

【推薦】 一個内部增長案例的分享

【推薦】 項目前端打包工具從 NEJ 切換成 webpack

繼續閱讀