DEKL 2.0: Trace-Indexed Knowledge Evolution in Dependent Type Theory
Abstract
DEKL 2.0 is a dependent type-theoretic framework for trace-indexed knowledge evolution. Its central claim is that the proof calculus remains monotone under standard structural rules, while non-monotonic behavior arises semantically from trace extension. Finite and infinite traces are first-class objects in the computational universe; knowledge is interpreted as a presheaf over the finite-trace category; and proposition-level reasoning is handled categorically with fixed-point support. We establish trace--reachability correspondence and completeness, characterize non-monotonicity by non-surjective restriction maps, and present a semantic interpretation based on the free category generated by a transition system. The framework unifies executable traces, typed witnesses, and knowledge revision in one dependent language.
Keywords
Cite
@article{arxiv.2604.22530,
title = {DEKL 2.0: Trace-Indexed Knowledge Evolution in Dependent Type Theory},
author = {Chen Peng},
journal= {arXiv preprint arXiv:2604.22530},
year = {2026}
}