nLab computational consistency



Computational consistency of a formal system says that

If the sequent e:(x 1=x 2)\vdash e \colon (x_1 = x_2) is derivable (claiming a witness of the proposition of equality of two terms) then the terms x 1x_1 and x 2x_2 have the same value by computation.

(Miquel, p.38)


Created on November 30, 2012 at 03:32:51. See the history of this page for a list of all contributions to it.