Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $$s(s(0))+ s(0)$$ to $$s(s(s(0)))$$ and it acts exactly and can be considered same as definitional equality (at least in type theory).

But then if we consider $$p$$ in $$p:Id_\mathbb{N}(a+b, b+a)$$ as computation steps taking $$a+b$$ to $$b+a$$ then what is the difference between computation steps in $$p$$ and computation steps in above mentioned computational equality which prevents $$p$$ to be considered sort of a definitional equality? Are they of different computation level/form?

Or in other words, if I have got it correctly, what is the difference between $$p$$ in $$p:Id_\mathbb{N}(a+b, b+a)$$ and $$p'$$ in $$p':Id_\mathbb{N}(s(s(0))+s(0), s(s(s(0))))$$ so that one can be considered almost the same thing as definitional equality but not the other one?

As an example following are the Agda codes in proving above mentioned reactions from Programming language foundations in Agda: Natural Numbers and [Programming language foundations in Agda: Proof by induction][3]correspondingly:

_ : 2 + 3 ≡ 5
=
-
begin
2+3
≡⟨⟩    -- is shorthand for
(suc (suc zero)) + (suc (suc (suc zero)))
≡⟨⟩    -- inductive case
suc ((suc zero) + (suc (suc (suc zero))))
≡⟨⟩    -- inductive case
suc (suc (zero + (suc (suc (suc zero)))))
≡⟨⟩    -- base case
suc (suc (suc (suc (suc zero))))
≡⟨⟩    -- is longhand for
5
∎


+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
begin
m + zero
≡⟨ +-identityʳ m ⟩
m
≡⟨⟩
zero + m
∎
+-comm m (suc n) =
begin
m + suc n
≡⟨ +-suc m n ⟩
suc (m + n)
≡⟨ cong suc (+-comm m n) ⟩
suc (n + m)
≡⟨⟩
suc n + m
∎


In my understanding both thing are computational steps that take you from left hand side to the right hand side!

P.S. I found the following piece in Homotopy Type Theory(§1.1 p.22) which I thought might be the answer to part of my own question:

Whether or not two expressions are equal by definition is just a matter of expanding out the definitions; in particular, it is algorithmically decidable (though the algorithm is necessarily meta-theoretic, not internal to the theory).

I guess the above paragraph is talking about $$\alpha$$ and $$\beta$$ expansions. But if that is true then it raises the question that: What does a proof of a proposition has in addition to function application that makes it a different equality? Is it that beside application we do have function definitions as well in a proof definition?!

• Please do not post images of formulas in your question. I can answer the question, but will do so after you've replaced the images with text. You can use the Markdown to show nice code. – Andrej Bauer Aug 13 at 7:47
• @Andrej Sorry about that. I thought I would post the image so that it keeps the color coding. Anyway I fixed it. Also meanwhile I had found something in HoTT book that I thought might be related to my question which I have added to the bottom of my question. Thanks in advance. – al pal Aug 13 at 15:46

What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $$a$$ and $$b$$, it normalizes both of them (based on judgemental equalities, such as $$\beta$$-reduction) and compares the normalized values for syntactic equalities. There is a theorem which says that $$a$$ and $$b$$ are judgementally equal if, and only if, they have syntactically equal normal forms.

When judgemental equality has the property that things are equal preciely when they have syntactically equal normal forms, then people sometimes call it computational equality because it "computes" by computing normal forms. There is a lot of confusion in terminology.

To test judgmental equality in Agda, we can use refl to show that two things are judgmentally equal (because the rule for refl states that refl a has type b ≡ c if, and only if, b and c are both judgmentally equal to a). Here are some examples:

 open import Relation.Binary.PropositionalEquality
open import Data.Nat

-- this works, the normal form of 2 + 3 is 5
p : 2 + 3 ≡ 5
p = refl

-- this works, the normal form of 0 + m is m
q : ∀ m → 0 + m ≡ m
q _ = refl

-- this does not work, because hte normal form of m + 0 is m
-- r : ∀ m → m + 0 ≡ m
-- r _ = refl


You can also show that $$2 + 3 = 5$$ by providing an element p' of 2 + 3 ≡ 5 which is not refl, such as the one you posted in the question. In the text you read, they were just trying to demonstrate the normalization steps by making them explicit as elements of an identity type (without saying so explicitly, probably). The thing to remember is that in Agda you will never see "a proof of judgemental equality", as that always happens in the background.

• Agda normalizes also by using inductive definitions, so the pseudo-code would look exactly like what you showed in your question. – Andrej Bauer Aug 14 at 17:17
• The second one ($m + n \equiv n + m$) does not work because in that case $m$ is a variable, but the inductive definition of $+$ has two clauses that specify what to do if the first arguments is $0$ and what to do if the first arguments is a successor. A variable $m$ is neither of those (Agda uses syntactic equality to figure out which inductive clause to use). – Andrej Bauer Aug 14 at 17:19
• Note that Agda normalizes suc m + n to suc (m + n) because it can use one of the inductive clasues, as the first argument is a successor. But it normalizes m + suc n to m + suc n because the inductive definition looks only at the first argument. – Andrej Bauer Aug 14 at 17:20
• While it is true that every closed term of type nat is of the form 0 or suc m, this is not the case for terms with open variables. For instance, given a variable k : nat can you tell me whether if k > 10 then 0 else 3 is of this form? What if we have a variable f : nat -> nat -> nat, and we consider the term f 4 2, is it 0 or suc n? I am not asking whether in some particular model of type theory numbers are zero or successors. I am asking whether these expressions can be shown to be equal to 0 or a successor in type theory (because that is what matters for Agda). – Andrej Bauer Aug 15 at 7:14
• Now, you could answer, for instance, that f 4 2 is equal either to 0 or to suc n but that does not tell us wich of the two options holds. You could keep pushing and do case-splitting of normalization, where you have two branches, one for f 4 2 = 0 and the other for f 4 2 = suc n, except that now you have to carry around arbitrary assumed equations while you perform normalization. Also note that the second option is not f 4 2 = suc n but rather ∃ (n : N) f 4 2 = n or something like that. It's just not going to work. – Andrej Bauer Aug 15 at 7:16