有件事情必须分清楚，程式语言上的函数，并不等同于数学上函数。
再来是实作跟语言也必须搞清楚，程式语言通常只规范，
但不说明该如何实作，虽然两者通常都有关系。
因此，若是只看待 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+