引用透明性

計算機科學中,引用透明性引用不透明性是部分電腦程式具有的屬性。若一個表達式在被其相應的值替換時能不改變程序的行為(反之亦然),則該表達式是引用透明的。 [1]因此,該表達式必須是純函數——給予相同的輸入,其返回值必須相同;對其求值時不能含有副作用。反之,一個不具有應用透明性的表達式是引用不透明的。

數學中,根據構成數學函數的定義,所有函數應用都是引用透明的。然而,在編程中情況並非總是如此;為避免歧義,函數經常被歸類為過程方法函數式編程的一個定義特徵是它只允許引用透明的函數。一些其他程式語言有提供方法用以選擇地保證引用透明性。一些函數式程式語言要求所有函數必須引用透明。

引用透明性的重要性在於允許程式設計師編譯器將程序行為作為重寫邏輯進行推理。這有助於證明正確性、簡化算法、在不破壞代碼的情況下協助修改代碼,以及通過記憶公共子表達式消除惰性求值並行計算來優化代碼。

歷史

應用透明性的概念據稱起源於阿爾弗雷德·諾斯·懷特海伯特蘭·羅素《數學原理》(1910–1913年)。 [2]它被威拉德·范·奧曼·蒯因引入分析哲學。在《詞與物》(1960年)第30章中,蒯因給出了如下定義:

如果一個包含模式 φ 是引用透明的,那麼當特指項 t 在一個術語或句子 ψ(t) 中是純粹引用的時候,其在包含術語或句子 φ(ψ(t)) 中也是純粹引用的。

該術語出現在其當代計算機科學用法中,在程式語言中對變量的討論中,在Christopher Strachey的開創性講義集《程式語言中的基本概念》(1967 年)中。講義引用了蒯因《詞與物》

例子和反例

如果表達式中涉及的所有函數都是純函數,則該表達式是引用透明的。

假設有函數可以從某個來源接受輸入並將其返回。在偽代碼中,該函數可能以GetInput(Source)調用,其中Source為特定的磁盤文件、鍵盤等的標識。在多次應用GetInput的情況下,即使Source一致,連續的返回值也會不同。因此,函數GetInput既不是確定性的,也不是引用透明的。

一個更為微妙的例子是使函數可以具有自由變量,即某些未被明確作為參數傳遞的輸入;然後根據名稱綁定規則將其解析為非局部變量,例如全局變量、當前執行環境中的變量(用於動態綁定)或閉包中的變量(用於靜態綁定)。由於可以在不更改作為參數傳遞的原值的情況下更改此變量,因此即便參數相同,後續調用該函數的結果也可能不同。然而,在純函數式編程中,破壞性賦值是不允許的,因此如果自由變量被靜態綁定到一個值,該函數仍是引用透明的,因為非局部變量及其值都分別由於靜態綁定和不可變性而不可改變。

算術運算是引用透明的:5 * 5可以替換為25。事實上,數學意義上的所有函數都是引用透明的:sin(x)是透明的,因為它總是對每個特定的x給出相同的結果。

重新賦值是不透明的。例如,C語言表達式x = x + 1更改了賦給變量x的值。在x最初為10的情況下,對該表達式連續求值兩次會分別得出1112 。顯然,將x = x + 1替換為1112時程序會具有不同含義,因此該表達式並不引用透明。但是,函數如int plusone(int x) { return x + 1; }透明的,因為輸入x不會被隱式變更 ,因此不含有如此副作用

today()不是透明的,當對它求值並以結果(比如, "Jan 1, 2001" )進行替換時,你不會得到與明天運行它得到的相同的結果。這是因為它取決於狀態(日期)。

在無副作用的語言,例如Haskell中,我們可以「用等於代替等於」:若 x == y,則有f(x) == f(y)。這反映了不可分者同一性原理。對於副作用語言,該屬性一般不需要成立。即便如此,重要的是將此類斷言限制為所謂的判斷相等性,即系統測試的術語相等性,不包括用戶定義的類型等價性。例如,如果B f(A x)和類型A已經覆蓋了相等性的概念,例如使所有項相等,那麼在x == y時仍有f(x) != f(y) 。這是因為像Haskell這樣的系統不會驗證在具有用戶定義的等價關係的類型上定義的函數是否在該等價方面得到了良好的定義。因此,引用透明性僅限於沒有等價關係的類型。將引用透明性擴展到用戶定義的等價關係可以通過例如 Martin-Löf 身份類型來完成,但需要依賴類型的系統,例如AgdaCoqIdris

與命令式編程對比

如果用其值替換表達式僅在程序執行的某個時刻有效,則該表達式不是引用透明的。這些序列點的定義和排序是命令式編程的理論基礎,也是命令式程式語言語義的一部分。

然而,因為引用透明的表達式可以在任何時候求值,所以不需要定義序列點,也不需要任何求值順序的保證。不考慮這些因素而完成的編程稱為純函數式編程

以引用透明的方式編寫代碼的一個優點是靜態代碼分析對一個智能編譯器會更容易,並且可以自動進行更好的代碼改進轉換。例如,在使用 C 語言編程時,如果在循環內包含對昂貴函數的調用,則會導致性能下降,即使可以在不更改程序結果的情況下將函數調用移出循環。程式設計師此時將被迫執行調用的手動代碼移動,但這可能會以犧牲原始碼的可讀性為代價。但是,如果編譯器能夠確定函數調用是引用透明的,它可以自動執行此轉換。

強制引用透明性的語言的主要缺點是它們使自然適合步驟序列命令式編程風格的操作的表達更加笨拙和不夠簡潔。這些語言通常包含使這些任務更容易的機制,同時保留語言的純功能質量,例如定字句語法和單子

又例

有兩個函數,一個是引用透明的(rt),另一個是引用不透明的(ro):

int g = 0;

int rt(int x) {
  return x + 1;
}

int ro(int x) {
  g++;
  return x + g;
}

函數rt是引用透明的,這意味着若x == y則有rt(x) == rt(y) 。例如, rt(6) = 7 。但是,我們不能確定ro同樣引用透明,因為它使用了由它自己修改的全局變量。 ro的引用不透明性使得對程序的推理更加困難。假設我們希望對以下陳述進行推理:

int i = ro(x) + ro(y) * (ro(x) - ro(x));

人們可能會想將這一陳述簡化為:

int i = ro(x) + ro(y) * 0;
int i = ro(x) + 0;
int i = ro(x);

然而這並不正確,因為ro(x)每次都會計算出不同的值。需要注意的是, ro的返回值基於未傳入的全局值g,並且每次調用rog都會被修改。這意味着數學恆等式xx = 0在此不有效,而是適用於像rt這樣引用透明的函數。


但是,可以使用更複雜的分析來將語句簡化為:

int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (x + tmp + 3 - (x + tmp + 4)); g = g + 4;
int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (x + tmp + 3 - x - tmp - 4)); g = g + 4;
int tmp = g; int i = x + tmp + 1 + (y + tmp + 2) * (-1); g = g + 4;
int tmp = g; int i = x + tmp + 1 - y - tmp - 2; g = g + 4;
int i = x - y - 1; g = g + 4;

這需要更多步驟,並且要求程式設計師對編譯器優化不可行的代碼有一定程度的洞察力。

因此,引用透明性使我們能夠推理我們的代碼,這將導致更健壯的程序,找到我們不希望通過測試找到的錯誤的可能性,以及看到優化機會的可能性。

另見

參考

  1. ^ John C. Mitchell. Concepts in Programming Languages. Cambridge University Press. 2002: 78. 
  2. ^ Alfred North Whitehead; Bertrand Russell. Principia Mathematica 1 2nd. Cambridge University Press. 1927.  Here: p.665. According to Quine, the term originates from there.

外部連結