邏輯式程式語言極簡實現(使用C#) - 4. 程式碼實現(完結)
阿新 • • 發佈:2020-07-06
本文是本系列的完結篇。本系列前面的文章:
* [邏輯式程式語言極簡實現(使用C#) - 1. 邏輯式程式語言介紹](https://www.cnblogs.com/skabyy/p/13199800.html)
* [邏輯式程式語言極簡實現(使用C#) - 2. 一道邏輯題:誰是凶手](https://www.cnblogs.com/skabyy/p/13199805.html)
* [邏輯式程式語言極簡實現(使用C#) - 3. 執行原理](https://www.cnblogs.com/skabyy/p/13209724.html)
下午,吃飽飯的老明和小皮,各拿著一杯剛買的咖啡回到會議室,開始了邏輯式程式語言的最後一課。
老明喝了一口咖啡,說:“你看咖啡機,是不是咖啡的列表。”
“啥?”小皮有點懵圈,“你說工廠的話還好理解,列表不太像。”
“每次點一下按鈕,就相當於呼叫了一次next,出來一杯咖啡。而它本身並不包含咖啡,每一次都是現場磨豆衝出來的。這正是一個典型的惰性列表。”
“有點道理,但是這跟邏輯式程式語言直譯器有什麼關係呢?”
“這就是下面要說的流計算模式,它是實現分支遍歷的核心技巧。”
下面先講流計算模式,然後再講替換求解的實現與分支遍歷的實現。
## 流(Stream)計算模式
老明在白板上寫下“Stream”,說:“Stream最常見的用途是用來表示數量未知或者無窮的列表。在程式碼中怎麼定義流呢?我們先來看看自然數,自然數是無窮的,那我們怎麼定義自然數列呢?”
“這很顯然,不就是0、1、2、3、4、5等等吧。”
老明鄙夷地看著小皮,說:“如果我是你的數學老師,那我肯定要罰你站在牆角數完所有自然數……想想數學歸納法!”
“哦哦,哎!數學這些烏漆嘛黑的知識總是喜歡偷偷溜走。自然數的定義簡單來說(~~嚴謹的不會~~),由兩部分組成:
1. (起點部分)0是自然數;
2. (遞迴部分)任意自然數加1也是自然數。
“這樣我們根據第1部分,得到起點0;再根據第2部分,一直加1,依次得到1、2、3、4、5等自然數。”
“看來基礎還是不錯的。”老明微笑著點點頭,然後開始進入正文……
從自然數的定義,我們可以得到啟發,**Stream的定義也是由兩部分組成**:
1. **起點**:第一個元素(非空流);
2. **遞迴**:一個無參函式,呼叫它會返回這個Stream去掉第一個元素後剩下部分組成的剩餘Stream。
**第2部分之所以是個函式,是為了獲得惰性的效果,僅當需要時才計算剩餘的Stream**。
使用程式碼定義Stream如下:
```CSharp
public delegate Stream DelayedStream();
// Stream的定義,我們只會用到替換的Stream,所以這裡就不做泛型了。
public class Stream
{
// 第一個元素,型別為Substitution(替換)
public Substitution Curr { get; set; }
// 獲取剩餘Stream的方法
public DelayedStream GetRest { get; set; }
private static Stream MakeStream(Substitution curr, DelayedStream getRest)
{
return new Stream()
{
Curr = curr,
GetRest = getRest
};
}
...
}
```
其中`Substitution`是替換類,後面會講到這個類的實現。
還需要定義一個空Stream,除了表示空以外,還用來作為有限Stream的結尾。空Stream是一個特殊的單例。
> 正常來講,空Stream應該額外宣告一個型別。這裡偷了個懶。
```CSharp
private Stream() { }
private static readonly Stream theEmptyStream = new Stream();
public bool IsEmpty()
{
return this == theEmptyStream;
}
public static Stream Empty()
{
return theEmptyStream;
}
```
特別的,還需要一個構造單元素的Stream的方法:
```CSharp
public static Stream Unit(Substitution sub)
{
return MakeStream(sub, () => Empty());
}
```
只有這些平凡的構造方法還看不出Stream的用處,接下來結合前面講過的NMiniKanren執行原理,探索如何使用Stream來實現替換的遍歷。
### Append方法
回顧一下`Any`的執行原理,`Any`的每個引數會各自返回一個Stream。這些Stream代表了各個引數包含的可能性。`Any`操作把所有可能性放在一起,也就是把這些Stream拼在一起組成一個長長的Stream。
![](https://img2020.cnblogs.com/blog/576869/202007/576869-20200703220124492-837914179.png)
所以相應的,我們需要把兩個Stream `s1`和`s2`拼接成一個“長”Stream的Append方法。
如何構造這個“長”Stream呢?
首先,如果`s1`是空Stream,那麼拼接後的Stream顯然就是`s2`。
否則,按照Stream定義,分兩個部分進行構造:
1. 第一個元素,顯然就是`s1`的第一個元素;
2. 剩餘Stream,就是`s1`的剩餘Stream,拼上`s2`,這裡是個遞迴定義。
按照上面分析的構造方法,我們就能輕鬆地寫下程式碼:
```CSharp
public Stream Append(DelayedStream f)
{
if (IsEmpty()) return f();
return MakeStream(Curr, () => GetRest().Append(f));
}
```
在這個實現中,`f`是尚未計算的`s2`。我們需要儘量推遲`s2`第一個元素的計算,因為推遲著推遲著可能就沒了不用算了。在很多場景中,這個可以節省不必要的計算,甚至避免死迴圈(“這都是血淚教訓。”老明捂臉)。
下面是一個`Any`與`Append`的例子:
![](https://img2020.cnblogs.com/blog/576869/202007/576869-20200703220144284-906903357.png)
### Interleave方法
`Anyi`和`Any`的區別只有順序。`Anyi`使用交替的順序。
所以相應的,我們需要一個方法,這個方法把兩個Stream `s1`和`s2`中的元素交替地拼接組成一個“長”Stream。
![](https://img2020.cnblogs.com/blog/576869/202007/576869-20200703220215332-78247956.png)
首先,如果`s1`是空Stream,那麼“長”Stream顯然就是`s2`。
否則,分兩部分構造:
1. 第一個元素是`s1`的第一個元素;
2. 這裡和Append方法的區別是把`s1`和`s2`的位置調換了,剩餘Stream是`s2`交替拼上`s1`的剩餘Stream,同樣是個遞迴定義。
程式碼如下:
```CSharp
public Stream Interleave(DelayedStream f)
{
if (IsEmpty()) return f();
return MakeStream(Curr, () => f().Interleave(GetRest));
}
```
這裡使用惰性的`f`是非常必要的,因為我們不希望取剩餘Stream的時候呼叫`GetRest`。
### Bind方法
這個方法比較複雜,是對應到`All`運算中兩兩組合引數裡的分支的過程。
![](https://img2020.cnblogs.com/blog/576869/202007/576869-20200703220233008-2077442312.png)
不同於`Append`/`Interleave`作用在兩個Stream上,`Bind`方法作用在一個Stream和一個Goal上。
為什麼不是兩個Stream呢?
前面已經分析過了,`k.All(g1, g2)`這個運算,是把`g2`蘊含的條件,追加到`g1`所包含的Stream中的每個替換裡。
同時,`g2`是個函式。追加這個動作本身由`g2`表達。
舉例來說,假設`st`是`g1`所包含的Stream中的一個替換。那麼把`g2`蘊含的條件追加到`st`上,其結果為`g2(st)`。
正是因為`Bind`方法中需要有追加條件這個動作,所以`Bind`方法的第二個引數只能是既包含了條件內容,也包含了追加方法的Goal型別。
用記號`s1`表示`g1`所包含的Stream,`Bind`方法的作用就是把`g2`蘊含的條件追加到`s1`中的每個替換裡。
首先,如果`s1`是個空Stream,那顯然`Bind`的結果是空Stream。
否則,結果是`s1`的第一個元素追加`g2`,再拼上`s1`的剩餘Stream `Bind` `g2`的結果。這仍是遞迴定義,不過是藉助的`Append`方法進行Stream構造。
程式碼如下:
```CSharp
public Stream Bind(Goal g)
{
if (IsEmpty()) return Empty();
return g(Curr).Append(() => GetRest().Bind(g));
}
```
> 這個方法為什麼叫`Bind`,因為取名廢只好抄《The Reasoned Schemer》裡的命名……
下面是一個`All`與`Bind`的例子:
![](https://img2020.cnblogs.com/blog/576869/202007/576869-20200703220251282-1271245918.png)
### Bindi方法
對應`Alli`,交替版的`Bind`方法。程式碼實現不再多說,直接把`Bind`實現中的`Append`換成`Interleave`即可:
```CSharp
public Stream Bindi(Goal g)
{
if (IsEmpty()) return Empty();
return g(Curr).Interleave(() => GetRest().Bindi(g));
}
```
> 更多Stream的玩法,參見《計算機程式的構造和解釋》(簡稱《SICP》)第三章。
## 替換求解的實現
構造目標時會用到替換裡的方法,所以和上一篇順序相反,先講替換求解。
### 替換
替換的定義為:
```CSharp
public class Substitution
{
private readonly Substitution parent;
public FreshVariable Var { get; }
public object Val { get; }
private Substitution(Substitution p, FreshVariable var, object val)
{
parent = p;
Var = var;
Val = val;
}
private static readonly Substitution theEmptySubstitution = new Substitution(null, null, null);
public static Substitution Empty()
{
return theEmptySubstitution;
}
public bool IsEmpty()
{
return this == theEmptySubstitution;
}
public Substitution Extend(FreshVariable var, object val)
{
return new Substitution(this, var, val);
}
public bool Find(FreshVariable var, out object val)
{
if (IsEmpty())
{
val = null;
return false;
}
if (Var == var)
{
val = Val;
return true;
}
return parent.Find(var, out val);
}
...
}
```
這是個單鏈表的結構。我們需要能在替換中追根溯源地查詢未知量的值的方法(也就是將條件代入到未知量):
```CSharp
public object Walk(object v)
{
if (v is KPair p)
{
return new KPair(Walk(p.Lhs), Walk(p.Rhs));
}
if (v is FreshVariable var && Find(var, out var val))
{
return Walk(val);
}
return v;
}
```
例如在替換`(x=1, q=(x y), y=x)`中,`Walk(q)`返回`(1 1)`。
注意替換結構裡面,條件都是`未知量 = 值`的形式。但是在NMiniKanren程式碼中並非所有條件都是這種形式。所以在追加條件時,需要先將條件轉化為`未知量 = 值`的形式。
追加條件時,不是簡單的使用`Extend`方法,而是用`Unify`方法。`Unify`方法結合了`Extend`和代入消元法。它先將已有條件代入到新條件中,然後再把代入後的新條件轉化為`未知量 = 值`的形式:
```CSharp
public Substitution Unify(object v1, object v2)
{
v1 = Walk(v1); // 使用已知條件代入到v1
v2 = Walk(v2); // 使用已知條件代入到v2
if (v1 is KPair p1 && v2 is KPair p2)
{
return Unify(p1.Lhs, p2.Lhs)?.Unify(p1.Rhs, p2.Rhs);
}
if (v1 is FreshVariable var1)
{
return Extend(var1, v2);
}
if (v2 is FreshVariable var2)
{
return Extend(var2, v1);
}
// 兩邊都是值。值相等的話替換不變;值不相等返回null表示矛盾。
if (v1 == null)
{
if (v2 == null) return this;
} else
{
if (v1.Equals(v2)) return this;
}
return null;
}
```
`Unify`方法實現了代入消元的第一遍代入(詳情見[上一篇](https://www.cnblogs.com/skabyy/p/13209724.html))。`Unify`的全拼是unification,中文叫合一。
### 求解
由於NMiniKanren的輸出只有未知量`q`,所以第二遍代入的過程只需要查詢`q`的值即可:
```CSharp
Walk(q)
```
## 構造目標的實現
通過Stream的分析,我們知道,只要構造了目標,自然就實現了分支的遍歷。
### Success與Fail
任何替換追加`Success`,相當於沒追加,所以`k.Success`直接返回一個只包含上下文的Stream:
```CSharp
public Goal Succeed = sub => Stream.Unit(sub);
```
任何替換追加`Fail`,那它這輩子就完了,`k.Fail`直接返回空Stream
```CSharp
public Goal Fail => sub => Stream.Empty();
```
### Eq
`k.Eq(v1, v2)`向上下文追加`v1 == v2`條件。
首先,使用`Unify`方法將`v1 == v2`條件擴充套件到上下文代表的替換。
若擴充套件後的替換出現矛盾,表示無解,返回空Stream。
否則返回只包含擴充套件後的替換的Stream。
程式碼如下:
```CSharp
public Goal Eq(object v1, object v2)
{
return sub =>
{
var u = sub.Unify(v1, v2);
if (u == null)
{
return Stream.Empty();
}
return Stream.Unit(u);
};
}
```
### Any/Anyi
首先,利用`Stream.Append`實現二目運算版本的`Or`:
```CSharp
public Goal Or(Goal g1, Goal g2)
{
return sub => g1(sub).Append(() => g2(sub));
}
```
然後擴充套件到多引數:
```CSharp
public Goal Any(params Goal[] gs)
{
if (gs.Length == 0) return Fail;
if (gs.Length == 1) return gs[0];
return Or(gs[0], Any(gs.Skip(1).ToArray()));
}
```
同理實現`Ori`和`Anyi`:
```CSharp
public Goal Ori(Goal g1, Goal g2)
{
return sub => g1(sub).Interleave(() => g2(sub));
}
public Goal Anyi(params Goal[] gs)
{
if (gs.Length == 0) return Fail;
if (gs.Length == 1) return gs[0];
return Ori(gs[0], Anyi(gs.Skip(1).ToArray()));
}
```
### All/Alli
利用`Stream.Bind`實現二目版本的`And`:
```CSharp
public Goal And(Goal g1, Goal g2)
{
return sub => g1(sub).Bind(g2);
}
```
然後擴充套件到多引數:
```CSharp
public Goal All(params Goal[] gs)
{
if (gs.Length == 0) return Succeed;
if (gs.Length == 1) return gs[0];
return And(gs[0], All(gs.Skip(1).ToArray()));
}
```
同理實現`Andi`和`Alli`:
```CSharp
public Goal Andi(Goal g1, Goal g2)
{
return sub => g1(sub).Bindi(g2);
}
public Goal Alli(params Goal[] gs)
{
if (gs.Length == 0) return Succeed;
if (gs.Length == 1) return gs[0];
return Andi(gs[0], All(gs.Skip(1).ToArray()));
}
```
## 串起來執行,以及一些細枝末節
```CSharp
public static IList