Document Open Access Logo

Towards Fuzzy Constructive Type Theories

Authors Besik Dundua , Furio Honsell , Temur Kutsia , Marina Lenisa , Luigi Liquori

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.7.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • Fuzzy type theory
  • constructive type theory
  • lambda calculus
  • residuated lattices

Metrics

Abstract

In this paper, we explore combinations of Fuzzy Logic and Constructive Higher Order Type Theory. Although Fuzzy Logic is more than 60 years old, and Fuzzy Type Theories have been studied in the classical case of Church’s Theory of Types, there is yet no satisfactory understanding of how to deal with judgements of the shape Γ⊢ M:_d A, where d is a fuzzy degree of confidence. Addressing this issue is important in view of the growing interest in quantitative and non-idempotent type theories. To this end, we introduce fuzzy type assignment systems in order to investigate how minimal fuzzy formulæbehave as types, according to some fuzzy proposition-as-types paradigm. Moreover, we study a fuzzy version of intersection types. In both systems assumptions are multisets and d, in Γ⊢ M:_d A, is a formula of minimal propositional Fuzzy Logic. Evaluating d in a residuated lattice [0,1], endowed with a left-continuous T-norm, we can analyse how the degree of confidence propagates from the assumptions to the conclusion, thereby yielding new information on the derivation. The former system sheds light on the connection between minimal Fuzzy Logics and affine λ-calculus and permits to show that the tautologies in the BCK-logic amount to the simple types which are inhabited by BCK-combinators. The latter system keeps track of the number of times a given fuzzy assumption is made. We discuss the standard suite of metatheorems (inversion lemmata and subject-conversion) for the systems, and point to possible uses of the fuzzy formula attached to the membership construct.

Cite As Get BibTex

Besik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, and Luigi Liquori. Towards Fuzzy Constructive Type Theories. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.7

Author Details

Besik Dundua
  • Giorgi Nikoladze Scientific-Research Center, Kutaisi International University, Georgia
  • Vekua Institute of Applied Mathematics, Tbilisi State University, Georgia
Furio Honsell
  • Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Udine University, Italy
Temur Kutsia
  • Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria
Marina Lenisa
  • Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Udine University, Italy
Luigi Liquori
  • Centre Inria de l'Université Côte d'Azur, Sophia Antipolis, France

Funding

Supported by the Austrian Science Fund (FWF) under project P 35530 and Shota Rustaveli National Science Foundation under project FR-25-5957.

Acknowledgements

The authors would like to express their gratitude to the reviewers for their precious comments on the original version of the present paper.

References

  1. Henk Barendregt. The Lambda Calculus - its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. URL: https://api.pageplace.de/preview/DT0400.9780080933757_A23543814/preview-9780080933757_A23543814.pdf.
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  3. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  4. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Inhabitation for non-idempotent intersection types. Logical Methods in Computer Science, 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:7)2018.
  5. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/JIGPAL/JZX018.
  6. Davide Castelnovo and Marino Miculan. Fuzzy algebraic theories. In Florin Manea and Alex Simpson, editors, CSL, volume 216 of LIPIcs, pages 13:1-13:17. Schloss Dagstuhl, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.13.
  7. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  8. Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini, and Furio Honsell. Sensible intersection type theories. In Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani, and Ugo de'Liguoro, editors, Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday, volume 441 of EPTCS, pages 126-147, 2026. URL: https://doi.org/10.4204/EPTCS.441.8.
  9. Erwin Engeler. Algebras and combinators. Algebra Universalis, 13:389-392, 1981. URL: https://doi.org/10.1007/BF02483849.
  10. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, TACS, volume 789 of LNCS, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  11. Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On quantitative algebraic higher-order theories. In Amy P. Felty, editor, FSCD, volume 228 of LIPIcs, pages 4:1-4:18. Schloss Dagstuhl, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.4.
  12. George Metcalfe. Fundamentals of fuzzy logic, 2005. URL: https://www.logic.at/tbilisi05/Metcalfe-notes.pdf.
  13. Vilém Novák. On fuzzy type theory. Fuzzy Sets Syst., 149(2):235-273, 2005. URL: https://doi.org/10.1016/J.FSS.2004.03.027.
  14. Rostislav Horčík. Petr Cintula, Petr Hájek. Formal systems of fuzzy logic and their fragments. Annals of Pure and Applied Logic, 150:49-72, 2007. URL: https://doi.org/10.1016/j.apal.2007.07.004.
  15. Sorites paradox. URL: https://plato.stanford.edu/entries/sorites-paradox/.
  16. Lotfi A. Zadeh. Fuzzy sets. Information and Control, 8(3):338-353, June 1965. URL: https://doi.org/10.1016/s0019-9958(65)90241-x.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact