To adopt proof assistants based on logic of total functions in education, one major problem is that of representing partial functions. In particular, one wishes to capture undefinedness in a rigorous way, while staying as close as possible to traditional mathematical practice. In this paper, we propose to represent potentially undefined terms with partial setoids on lifted terms, and to understand book equalities occurring in equality chains as special directed relations that hold only under assumptions of definedness for some terms. We also employ a suitable notion of strict morphism to fully automate propagation of these directed relations in strict contexts.
C. Sacerdoti Coen, E. Zoli (2007). A Note on Formalizing Undefined Terms in Real Analysis. s.l : s.n.
A Note on Formalizing Undefined Terms in Real Analysis
SACERDOTI COEN, CLAUDIO;ZOLI, ENRICO
2007
Abstract
To adopt proof assistants based on logic of total functions in education, one major problem is that of representing partial functions. In particular, one wishes to capture undefinedness in a rigorous way, while staying as close as possible to traditional mathematical practice. In this paper, we propose to represent potentially undefined terms with partial setoids on lifted terms, and to understand book equalities occurring in equality chains as special directed relations that hold only under assumptions of definedness for some terms. We also employ a suitable notion of strict morphism to fully automate propagation of these directed relations in strict contexts.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.