2026-07-30T13:55:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27025 2026-07-30T09:16:25Z ddc:004 open_access

Towards Fuzzy Constructive Type Theories Dundua, Besik Honsell, Furio Kutsia, Temur Lenisa, Marina Liquori, Luigi Fuzzy type theory constructive type theory lambda calculus residuated lattices 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Besik Dundua and Furio Honsell and Temur Kutsia and Marina Lenisa and Luigi Liquori 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.7 urn:nbn:de:0030-drops-270256 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.7 eng https://creativecommons.org/licenses/by/4.0/legalcode