有件事情必須分清楚，程式語言上的函數，並不等同於數學上函數。
再來是實作跟語言也必須搞清楚，程式語言通常只規範，
但不說明該如何實作，雖然兩者通常都有關係。
因此，若是只看待 Agda 這個例子，if 是直接被定義為
語言內的函數，因此 if 的確是個函數。如果仔細看這個語言，
會發現語言定義的內容極為精簡，包括連整數都是透過
inductive data types 在「語言之內」定義出來，
沒有所謂的 primitive data type 。
既然他是程式語言上的函數，那每個函數是不是能夠對應一個
數學上的函數呢？那我們就必須把語言每個組件都對應到數學結構上，
data type 必須要有對應的數學結構，這樣才能說明函數的是什麼。
因為在 Agda 上有 termination checker，可以保證每個語言上的函數，
給定輸入就有輸出。雖然這語言具備 dependent type，但若只考慮
simple type 的部分，每個 data type D 可以單純地對應一個集合 D'。
對於 f : D -> E 上 Agda 的函數，
配合 termination checker，f(x) 必然回傳 E 上的資料。
因此 D -> E 的 Agda 函數則對應 D' -> E' 上的集合函數。
若考慮有 side-effect 的語言，為了說明把問題簡化一下，
我們考慮一個語言僅有 global variable, 沒有 exception, 變數名稱僅由英文字母組成,
不考慮如何分析語法的問題，程式僅由 statement 與 expression
（無限整數以及其操作）也沒有任何自行宣告或定義的函數等。
（所以這是一個沒有函數的語言）
在這語言內唯一會改變變數的值的 statement ，只有 assignment, =
然後也僅有 Boolean type。這可能稱不上一個有用的程式語言，但為了說明這已經夠了。
語法就像這樣
statement = {statement} | statement ; statement | skip
if (expression) then statement else statement | variable = expression
既然我們考慮的變數名稱僅以英文字母 EN = {a, ... z, A, ..., Z} 組成，
我們寫 EN+ 代表所有長度不為零的有限字串集合，有限字串在數學中可以用有限序列
也就是 N| -> EN 的函數來表達，其中 N| 代表 {0, ..., N-1} 的集合。
而每個變數名稱與一個值連繫在一起，可能是 true, false 或是 undefined，
（我並沒有說每個值預設為 undefined，這在這邊不重要）
那麼，實際上程式的狀態是代表一個函數 s : EN+