Probabilistic Typed Natural Deduction for Trustworthy Computations Fabio A. D’Asaro Giuseppe Primiero Department of Philosophy Department of Philosophy “Piero Martinetti”, “Piero Martinetti”, University of Milan, Italy University of Milan, Italy fabio.dasaro@unimi.it giuseppe.primiero@unimi.it Abstract In this paper we present a typed natural deduction calculus to analyze the formal design of probabilistic computational processes, e.g. in use in machine learning techniques, to model their trustworthiness as a safety property. 1 Introduction In this paper we introduce a natural deduction derivation system dubbed Trustworthy Probabilistic Typed Natural Deduction (TPTND for short). The aim of this system is to automatize the task of reasoning about computational processes with probabilistic outputs. In particular, we model computational processes as (generalized) Bernoulli random variables from which we draw a number of independent samples. We interpret the latter as independent runs of the process, and we refer to them as experiments. This allows us to derive properties of these processes, and in particular to verify their trustworthiness. The latter is modelled as a form of statistical hypothesis testing, and it is intended as the acceptable distance of the probabilistic value of the output of an experiment from the value intended by the relevant distribution. Our framework uses typed sequent calculus-style judgements, where the context of derivation can be intuitively interpreted as representing a probability distribution, and the derived formula as a series of samples extracted from such distribution. Types and terms of our calculus are decorated with an empirical probability and a sample size respectively. For example, the TPTND judgement Γ $ toss100 : Heads 0.35 may be interpreted as the statement that, under distribution Γ, tossing a coin 100 times produced output Heads 35% of the times. Γ will specify the value assigned to the output of each random variable of interest to the experiment of tossing a coin, and in particular whether one is assuming that the coin is fair or biased. It is under such assumption that one wants to judge the trustworthiness of the process at hand, e.g. we may ask whether the toss process follows a fair distribution over the outcomes Heads and T ails. In particular, assuming that Γ expresses the distribution corresponding to a fair coin as the possible outputs declaration of one random variable Γ “ tx : Heads0.5 , x : T ails0.5 u, the process toss should be considered trustworthy if increasing the number n of its runs, the probability of output Heads gets arbitrarily closer to 0.5. An experiment in TPTND corresponds Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). In: R. Falcone, J. Zhang, and D. Wang (eds.): Proceedings of the 22nd International Workshop on Trust in Agent Societies, London, UK on May 3-7, 2021, published at http://ceur-ws.org 1 to the basic syntactic transformation of a term increasing its sample size from n to n ` 1. Generalizing from this toy example, any probabilistic computation can be understood as trustworthy in this sense, and therefore our system can be applied to verify trust in e.g. classifiers to produce the correct output. As standard for type systems, a soundness result is formulated in terms of type safety, which for TPTND establishes that the syntactic transformations of computational processes allowed in the system 1. do not permit to output unintended results (read: side-effects); and 2. provide the means to assess whether a computation is trustworthy, namely if after a (sufficient) number of executions the probabilistic value of the current output approximates the one intended by the corresponding distribution. In our example, if the distance of the current output Heads0.35 from the value Heads0.50 assigned in the distribution decreases as a function of n execution of the process toss, we say that this process is trustworthy. We consider this system a useful step towards the formal design and automatization of reasoning about probabilistic computations like those in use in machine learning techniques, as well as for the development of proof-checking protocols on such computational systems. In the following, we show the internal workings of TPTND by extending a simple die rolling example. However, we also hint at concrete applications using a more realistic example inspired by gender-bias verification. The remainder of this paper is organised as follows. In Section 2 we briefly overview some of the most relevant related works in the area of probabilistic type and natural deduction systems, as well as in the area of computational trust using such logical tools. In Section 3 we introduce TPTND through its language, its rules and its structural properties. In Section 4 we provide a series of examples to show the functioning of the system. In Section 5 we offer meta-theoretical results leading to the formulation of safety illustrated above. Finally in Section 6 we sumamrize and sketch the next steps of this research. 2 Related Work The extension of type systems with probabilities has been recently explored in the literature. Similarly to our work, [Pie20], [Bor19], [GIK` 18] introduce some form of probability in calculi with types or natural deduction systems. [Pie20] introduces a λ-calculus augmented with special “probabilistic choice” constructs, i.e. terms of the form M “ tp1 M1 , . . . , pn Mn u, meaning that term M has probability p1 , . . . , pn of reducing to one of the terms M1 , . . . , Mn respectively. Unlike TPTND, [Pie20] deals with judgements that do not have a context and uses a subtyping relation for the term reduction. [Bor19] introduces “probabilistic sequents” of the form Γ $ba ∆ that are interpreted as empirical statements of the form “the probability of Γ $ ∆ lies in the interval ra, bs”. Differently from this work, TPTND does not express explicitly probabilistic intervals, but only sharp probability values, while at the same time expressing such probability on output types, rather than on the derivability relation. Finally, [GIK` 18] introduces the logic PΛÑ where it is possible to mix “basic” and “probabilistic” formulas, the former being similar to standard Boolean formulas, and the latter being formed starting from the concept of a “probabilsitic operator” Pěs M : σ stating that the probability of M : σ is equal to or greater than s. The semantics for PΛÑ is Kripke-like and its axiomatisation is infinitary. TPTND offers an integrated way to deal with probability intervals (similarly to [GIK` 18]) and probabilistic choices (similarly to [Pie20]). However, unlike these languages, TPTND was mainly designed to reason about and derive trustworthiness properties of computational processes. In fact, differently from all these other systems, TPTND has an explicit syntax both to deal with the number of experiments, and to prove trust in a process whenever the empirically verified probability is close enough to the theoretical one. The application of TPTND is specifically targeted to the evaluation of trustworthiness of probabilistic computational processes. The literature offers several logical frameworks providing a computational no- tion of trust which deals with one of its many aspects, from manipulation to verification to assessment [Dem04, Sin11, DBS17, Ald18, AT19, DQBS20]. Modal logics, and in particular knowledge and belief log- ics, have been extensively investigated for trust, see e.g. [Lia03, HLHV10, LL17]. Much less investigated are proof systems for trust. An exception is the family of logic (un)SecureND whose most complete formu- lation, including also a relational semantics, is offered in [Pri20]. The proof-theoretic fragment of the logic has been applied to: software management [BPR15, PB17, PB18] including a Coq implementation (https: 2 ř base Γ $ tn : αa a` x:βb PΓ b ď 1 tu :: distribution extend Γ, x : αa :: distribution Figure 1: Distribution Formation Rules exp (where ã „ Bpa, nq) Γ, x : αa $ tn : αã Γ $ tn : αã Γ $ tm : αã1 IK upd Γ $ tn : K0 Γ $ tn`m : αã˚pn{pn`mqq`ã1 ˚pm{pn`mqq Figure 2: Rules of Calculus //github.com/gprimiero/SecureNDC); modelling a trust and reputation protocol for VANET [PRCN17]; and the evaluation of the trustworthiness of online sources [CP19]. The system TPTND presented in this paper can be seen as the probabilistic extension of the fragment of (un)SecureND including only the closure of trust under negation which corresponds to distrust in the latter system. 3 TPTND 3.1 Syntax The syntax of TPTND is as follows: Definition 1 (Syntax). T :“ x | tn | xt, uyn | fstptqn | snd ptqn | rxstn | t.un O :“ αr | pα ˆ βqr | pα ` βqr | pα Ñ βqrr1 sr | Kr R :“ Γ; ¨ | Γ; x : αa S :“ Γ :: distribution Terms T are computational processes, including: variables, constants indexed by a natural number value, pairs of constants, a first and second projection function, an abstraction term and an application. In TPTND, terms with different names are regarded as independent processes. In the remainder of this paper, we assume that each process has its associated variable, e.g., t has variable xt (and vice versa). This is useful in particular to guarantee that distinct processes (possibly with the same outputs) are used correctly in the construction of a distribution. However, to simplify notation, we do not decorate variables with subscripts unless necessary. Thus, throughout we implicitly assume that, whenever a process and a variable occur in an expression, they correspond to each other. Types O, deviating from the standard interpretation, are output values with a probability r P r0, 1s attached: α is a meta-variable for the output of a computational process; α ˆ β is the independent occurrence of outputs α and β; α ` β is the disjunction of outputs α and β; α Ñ β expresses output type β as a function of α: in this case the probability value is itself the probability r of β given the probability r1 of α, and its meaning is explained by substituting to the latter an empirically determined probability value for a process whose output is α; we use K to denote "no output" or a non-termination condition. Contexts R are coherent probability distributions, composed by expressions of the form x : αa . For instance, the context tx : Heads 1{2 , x : Tails 1{2 , y : Heads 1{3 , y : Heads 2{3 u defines two independent random variables x and y which may be intuitively interpreted as a fair and biased coin respectively. Type declarations S include statements of the form Γ :: distribution expressing that that Γ is a validly defined distribution. Judgements in TPTND have the form Γ $ tn : αã saying that under a coherent probability distribution, encoded in Γ, a given process t has empirical probability ã to produce an output of type α after a sample of n of experiments. Intuitively, we can interpret $ as the process of extracting n samples from the categorical distribution Γ and getting n ˆ r a times output α. Note that we use the notation ã to denote an empirical probability, as opposed to its theoretical probability counterpart which we simply denote as a. Table 1 summarizes the main notational conventions used throughout the paper. 3 Symbol(s) Meaning/Used for: t, u, t1 , u1 . . . Processes x, y, x1 , y 1 , . . . Variables α, β, α1 , β 1 , . . . Output types a, b, a1 , b1 , . . . Probabilities (Real numbers in r0, 1s) a, rb, ar1 , br1 , . . . r Empirical probabilities (Real numbers in r0, 1s) n, n1 , . . . Natural numbers (usually representing sample size) x : αa Variable x gives output α with probability a tn : αar n executions of process t give output α with empirical probability r a Γ, ∆, Γ1 , ∆1 , . . . Contexts defining probability distributions, i.e., sets of the form tx : αa , x1 : αa1 1 , . . . u Γ $ tn : αar Sampling from probability distribution in Γ results in tn : αar rasb Value b depends on a ra1 {asb Substitution of a1 to a in b x¨, ¨y, f st, snd, λ Symbols to compose processes ˆ, `, Ñ Symbols to compose types Table 1: Notation Γ $ tn : αã ∆ $ um : βb̃ t‰u Γ $ tn : αã Γ $ tn : βb̃ Iˆ I` Γ, ∆ $ xt, uyn¨m : pα ˆ βqã˚b̃ Γ $ tn : pα ` βqã`b̃ Γ $ tn : pα ˆ βqc̃ Γ $ fstptqm : αã Γ $ tn : pα ˆ βqc̃ Γ $ snd ptqm : βb̃ EˆL EˆR Γ $ snd ptqn{m : βc̃{ã Γ $ fstptqn{m : αc̃{b̃ Γ $ tn : pα ` βqc̃ Γ $ tn : αã Γ $ tn : pα ` βqc̃ Γ $ tn : βb̃ E`L E`R Γ $ tn : βc̃´ã Γ $ tn : βc̃´b̃ Γ, x : αa $ tn : βb̃ Γ $ rxstn : pα Ñ βqrasb̃ ∆ $ um : αã IÑ EÑ Γ $ rxstn : pα Ñ βqrasb̃ Γ, ∆ $ pt.uqn : βrã{asb̃ Figure 3: Rules for Connectives 3.2 Typing Rules In this section we present the rules of TPTND. In Figure 1 we show the formation rules for the probability distribution. Contexts are built inductively. We start from an empty context (rule “base”), and can extend it with x : αa whenever we are provided with an estimate a for the probability of output α (rule “extend”), provided the sum of probabilities over outputs for variable x does not exceed 1. In view of the association of processes and variables, it holds that, for any context Γ, a variable cannot yield a single output with two (or more) distinct probabilities. For instance, tx : Heads 1{2 , x : Heads 1{3 u is not a valid context. In particular, in the rule “extend” the process tn is meant to add the output α to the family of variables x : β, as indicated in the side condition of the rule. In addition, for any given variable x, the sum of the probabilities over its output types is always less or equal than 1, therefore e.g. tx : Heads 0.6 , x : Tails 0.7 u is not a valid context. In Figure 2 we present the basic derivation rules of the calculus. Given a categorical distribution, including a random variable which is assigned a probability a to output α, a term t has empirical probability ã to produce α after a sample of n of experiments (rule “exp”) where r a follows a Binomial distribution with parameters a Γ, x : αa :: distribution ∆ $ un : αã1 | a ´ ã1 |ď pnq IT Γ, ∆ $ Trustpun : αã1 q Γ, x : αa :: distribution ∆ $ un : αã1 | a ´ ã1 |ą pnq I T Γ, ∆ $ Trustpun : αã q Figure 4: Trust Fragment 4 and n (written Bpa, nq). Rule “upd” allows one to combine the empirical probabilities for two series of runs of a fixed process t. In fact, if n runs of process t produced output α with empirical probability r a and m runs produced output α with empirical probability ar1 , then it holds that n ` m runs produce output α with empirical probability given by the weighted sum of n and m over the total number of experiments. Recall that we regard the special type K as a the value associated to programs which do not terminate with a valid output. Rule “IK” formalizes the intuition which states that no process in the system of interest can produce output K, or in other words that we always assume termination. In Figure 3 we define rules for connectives. The typing rule Iˆ says that if two distinct (and thus independent) processes t and u produced empirical probabilities ã and b̃ for outputs α and β and sample sizes n and m respectively, the empirical probability of jointly getting output α and β from t and u is given by ã ˚ b̃. Note that in this rule, if we have n samples extracted from t and m from u, then the sample size increases to n ¨ m in the conclusion as we need to consider all possible pairs of outputs. By Eˆ, given a process for two independent outputs with associated probability c̃, and knowing the probability of the first composing process ã, we infer the probability of the second process to produce the second output as c̃{ã; the dual rule has snd in the second premise and f st in the conclusion. Example 1. Let d and g be two dice associated with distributions ∆ and Γ respectively. Rolling die d 4 times produces the series 1, 3, 5, 1. We also roll die g 6 times, producing 2, 3, 6, 1, 4, 4. In our syntax, this translates to ∆ $ d4 : 11{2 and Γ $ g6 : 21{6 . The empirical probability of getting a 1 from die d and a 2 from g can be estimated by considering all the pairs of rolls, i.e. the 24 pairs p1, 2q, p1, 3q, p1, 6q, p1, 1q, p1, 4q, p1, 4q, p3, 2q, p3, 3q, p3, 6q, p3, 1q, p3, 4q, p3, 4q, p5, 2q, p5, 3q, p5, 6q, p5, 1q, p5, 4q, p5, 4q, p1, 2q, p1, 3q, p1, 6q, p1, 1q, p1, 4q and p1, 4q. The pair p1, 2q occurs twice in the list – this is mirrored by our Iˆ rule: ∆ $ d4 : 11{2 Γ $ g6 : 21{6 Iˆ ∆, Γ $ xd, gy24 : p1 ˆ 2q1{12 Conversely, if we are told that the pair p1, 4q occurs 4 times in the list of 24 pairs of independent rolls of d and g, and that die g gave 4 on 2 rolls out of 5, then we can conclude that die d gave 1 on 2 rolls out of 4. In our calculus, this is formalized as: ∆, Γ $ xd, gy24 : p1 ˆ 4q4{24 ∆, Γ $ snd xd, gy6 : 42{6 EˆR ∆, Γ $ fstxd, gy4 : 11{2 Rule I` introduces disjunction: intuitively, if we have that process t produces outputs α and β with frequencies a and rb respectively, then the frequency of output α or output β is r r a ` rb. Rule IÑ introduces the implication by constructing the empirical probability of output β for process tn as a function of the theoretical probability a of α under context Γ. The empirical probability b̃ of β given the theoretical probability a of α is denoted rasrb. EÑ eliminates such dependency substituting the theoretical probability a with the empirical probability measured under context ∆ over m experiments. We denote such substitution by ra{r asrb. Note that the estimate of a does not need to be based on the same number of experiments as those run for rxstn . The conclusion provides an estimate of the empirical probability of process t outputting β when it is run n times, according to an estimate a obtained from m runs of process u outputting α. r 3.3 Trustworthy computations In Figure 4 we provide typing rules for trustworthy computations. A probabilistically valid output is labeled as trustworthy under a given distribution if and only if given the probability ã of producing a given output based on the known probability distribution, the computational process t after a sample of n experiments has probability ã1 to produce an output of type α such that the difference between ã and ã1 remains below a critical threshold, parametric with respect to the number of experiments performed (rule IT). If such a value is surpassed, the process is labelled untrustworthy (rule T). The parametric threshold pnq is domain-specific and depends on the application. For instance, one may take pnq to correspond to the 95% confidence interval under the Normal approximation to the Binomial Distribution. Note that, according to these rules, it is possible to derive the trustworthiness of some untrustworthy process (and vice versa) with some (very small) probability. The probability of this happening can be made arbitrarily small by repeating the experiment associated with the process. 5 3.4 Structural Rules Structural Rules are admissible. The Cut rule can be obtained as a detour of IÑ and EÑ as follows: ∆, x : αa $ un : βrb IÑ ∆ $ rxsun : pα Ñ βqrrasrb Γ $ tn : αar EÑ Γ, ∆ $ pu.tqn : βrra{rasrb Contraction would say that, given the empirical probability ra that process t outputs α determined over m experiments; and given the probability ar1 of an independent instance t1 to output α given n ą m experiments; the context in which the two processes are considered both can be contracted with a probability assigned to obtain α updated by rule “upd”. The rule can be obtained as a detour of Extend, Exp and upd: Γ $ tn : αã exp extend Γ, x : αa :: distribution Γ, x : αa $ tm : αã1 upd Γ $ tn`m : αã˚pn{pn`mqq`ã1 ˚pm{pn`mqq ext Γ, y : αã˚pn{pn`mqq`ã1 ˚pm{pn`mqq :: distribution Finally, consider that the rule upd is used to extend a distribution Γ, x : αa by the result of a new experiment ∆ $ tn : αã1 , i.e. where there is a confounder x : αa $ tn : αã1 . For any new process without such a condition, the rule Extend will act as Weakening. 4 Examples In this section, we illustrate the working of TPTND by commenting on a toy die-rolling example. Example 2. We first start by modeling a fair die. Let Γ “ tx : 11{6 , . . . , x : 21{6 , . . . , x : 61{6 u. Then, for example, we can construct a process that outputs type 5 or 6 with probability 2{6 as follows: exp exp Γ $ tn : 51{6 Ą Γ $ tn : 61{6 Ą I` Γ $ tn : p5 ` 6q2{6 Ą Now let ∆ be an “opaque” context, i.e. an unknown distribution. One of the use of our trust fragment is to allow reducing “opaque” contexts to “transparent” ones by verifying whether an empirical probability is sufficiently close to one we expect. In this sense, a trustworthy computation is one whose underlying distribution has been explained. The following example demonstrates this use of trust: Example 3. Let ∆ be an opaque context, i.e. a "die system" which we have been provided with; and let Γ be the distribution defined in Example 2, representing a fair die. In this example, we focus on output 5. Experimenting under context ∆ gives: exp ∆ $ u10 : 51{2 Our aim is to decide whether ∆ describes a fair distribution over outputs t1, 2, . . . , 6u, i.e. whether ∆ ap- proximates correctly to Γ and can be therefore considered safe to use. To this aim, we use the Introduction of (Negative) Trust, where we use the (exact) Binomial 95% confidence interval to set our threshold: Γ $ tn : 51{6 Ą ∆ $ u10 : 51{2 1{6 R r0.19, 0.81s I T Γ, ∆ $ Trustpu10 : 51{2 q that is, we do not trust process u to be extracted from the distribution Γ. Obviously, things may change as new evidence is collected, as we show in the following example: Example 4. Let Γ, ∆ be as in Examples 2 and 3, and suppose we are provided with some more experimental evidence about process u, i.e. ∆ $ u20 : 53{20 . We can use rule “upd” to update the result from Example 3: 6 ∆ $ u10 : 51{2 ∆ $ u20 : 53{20 upd ∆ $ u30 : 54{15 Γ, x : 51{6 :: distribution 1{6 P r0.12, 0.46s Γ, ∆ $ Trustpu30 : 54{15 q i.e., based on a total of 30 runs of process u, now we trust it to be extracted from the transparent and fair distribution Γ. We now turn to a gender-bias inspired example, where we test whether we trust a given classifier not to have an inherent bias. Example 5. Suppose we are given a commercial, closed-source software to automatically shortlist CVs according to a set of criteria. To this aim, we consider the output of the classification algorithm to fall into one of the following four categories: (1) male, shortlisted, (2) male, not shortlisted, (3) female, shortlisted, (4) female, not shortlisted. To verify that the underlying algorithm does not have an inherent gender bias, we test whether we trust the distribution over these four classes to reflect the actual gender distribution in the current Italian population, as encoded in a distribution Γ “extended” from an official dataset. A proof that this is indeed the case would produce a certificate in the form of a natural deduction proof, that would go as follows: $ populationn : female0.52 extend tx : female0.52 u :: distribution ∆ $ c10 : female3{10 0.52 P r0.07, 0.65s IT Γ, ∆ $ Trustpc10 : female3 q where we assumed a 95% confidence interval and n “ 62246674 is the Italian population in July 2018. Note that a shortlist selection which would provide strictly less than 2{10 or more than 9{10 of female candidates would be considered untrustworthy according to this model. Note that if we sampled 30 CVs instead, shortlisting 7 female CVs, we would derive untrustworthiness: $ populationn : female0.52 extend tx : female0.52 u :: distribution ∆ $ c30 : female7{30 0.52 R r0.1, 0.42s I T Γ, ∆ $ Trustpc30 : female7{10 q We would in fact consider untrustworthy any number of shortlisted female CVs strictly smaller than 10 or bigger than 21. We now show how our syntactic machinery allows for the definition of dependent processes: Example 6. Let Γ “ tx : 1x1 , . . . , x : 6x6 , y : 1y1 , . . . , y : 6y6 u be a distribution. Note that, according to axiom “extend”, x1 , . . . , x6 , y1 , . . . , y6 are variables in r0, 1s such that x1 ` ¨ ¨ ¨ ` x6 ď 1 and y1 ` ¨ ¨ ¨ ` y6 ď 1. Then, for any n P N, rule “exp” gives: exp exp Γ $ tn : 5xĂ5 Γ $ un : 5yĂ5 and exp exp Γ $ tn : 6xĂ6 Γ $ un : 6yĂ6 Applying the introduction of conjunction yields: Γ $ tn : 5xĂ5 Γ $ un : 6yĂ6 Iˆ Γ $ xt, uyn2 : p5 ˆ 6qxĂ5 ¨Ă y6 and Γ $ tn : 6xĂ6 Γ $ un : 5yĂ5 Iˆ Γ $ xt, uyn2 : p6 ˆ 5qxĂ6 ¨Ă y5 Finally, we can introduce disjunction: 7 Γ $ xt, uyn2 : p5 ˆ 6qxĂ6 ¨Ă y5 Γ $ xt, uyn2 : p6 ˆ 5qxĂ5 ¨Ă y6 I` Γ $ xt, uyn2 : pp5 ˆ 6q ` p6 ˆ 5qqxĂ5 ¨Ă y6 `x y5 Ă6 ¨Ă For readability, we rename the type pp5 ˆ 6q ` p6 ˆ 5qq into 11, since the type pp5 ˆ 6q ` p6 ˆ 5qq corresponds to the only way we can get the two dice to sum to 11. Under this convention, the latter conclusion reads: Γ $ xt, uyn2 : 11xĂ5 ¨Ă y6 `x y5 Ă6 ¨Ă Now we introduce Ñ: Γ, x : 5x5 $ xt, uyn2 : 11xĂ5 ¨Ă y6 `x y5 Ă6 ¨Ă IÑ Γ $ rxsxt, uyn2 : p5 Ñ 11qrx5 spxĂ5 ¨Ă y6 `x y5 q Ă6 ¨Ă Finally we illustrate elimination: Γ $ rxsxt, uyn2 : p5 Ñ 11qrx5 spxĂ5 ¨Ă y6 `x y5 q Ă6 ¨Ă ∆ $ vm : 50.99 EÑ Γ, ∆ $ pxt, uy.vqn2 : 110.99¨Ă y6 `x y5 Ă6 ¨Ă 5 Metatheory The meta-theoretical analysis of TPTND aims at proving type safety. Such result, in line with the traditional approach defined first in [WF94], is obtained by formulating type preservation in Theorem 3 and progress in Theorem 4. In TPTND these results are interpreted as follows: • preservation: any computation implementing certain steps preserves the probability of its intended output; • progress: any such computation is trustworthy, and viceversa. This interpretation of progress deviates from the standard one, which requires proving that for any term either a reduction step can be formulated, or the term is in normal form. In TPTND there is no restriction on the number of term transformation which can be performed by experiment execution, hence one can repeatedly apply the upd rule. To reach safety, we first formulate substitution (both deterministic and non-deterministic) and rules for term evaluation. Theorem 1 (Deterministic Substitution). If x : αa $ tn : βb˜1 and $ un : α1 , then $ pt.uqn : βb˜1 . Proof. By structural induction on the premise of the first derivation. To show the reduction to b1 , for each case of x : αa $ tn : βb˜1 in the induction, take the second derivation $ un : α1 , where the output α does not depend on any distribution, as additional premise in the elimination from $ rx{ustn : pα Ñ βqrasb to derive the term pt.uqn : βr1{asrb1 : • For α atomic, the case is immediate; • For α ” γ ˆ δ, there are independent terms xv, zyn such that: $ vn : γ1 , x : γ1 $ tn : βb1 and the base case applies; $ zn : δ1 , x : δ1 $ tn : βb1 and the base case applies; • For α ” γ ` δ, the term un is induced from un : γb˜2 and un : δb˜3 with b2 ` b4 “ 1; i.e., α is a metavariable for the distribution of possible outputs of the term u. Then either one of them is such that un : γ1 or un : δ1 (and respectively the other term has probability “ 0), then use distributivity of ` over Ñ and commutativity of ` to select either one, and the base case applies. • For α ” γ Ñ γ (as an instance of the rule upd), the term un is of the form rxsvn with output having b “ 1; hence, x : γ1 $ vn : γ1 and y : pγ Ñ γq1 $ tn : βb1 allows to derive $ t.un : βb1 ; In most interesting cases, substitution will make use of non-deterministic processes: 8 t1n tn ÞÑp t1n tn ÞÑp t1n tn ÞÑp t1n un ÞÑp u1n tn ÞÑp tn`1 f stptn q ÞÑp f stpt1n q sndptn q ÞÑp sndpt1n q xt, uyn ÞÑp xt1 , uyn xt, uyn ÞÑp xt, u1 yn t1n t1n tn ÞÑp t1n tn ÞÑp t1n tn ÞÑp t1n f stpxt, uyn q ÞÑp tn sndpxt, uyn q ÞÑp un rxstn ÞÑp rxst1n t.un ÞÑp t1 .un rx{tsun ÞÑp rx{t1 sun Figure 5: Term Evaluation Rules Theorem 2 (Non-deterministic Substitution). If x : αa $ tn : βb̃ , and Γ $ un : αãă1 , then Γ $ pt.uqn : βrb1 ă1 . Proof. By structural induction on the premise of the first derivation, as above to derive the term pt.uqn : βrra{asrb1 : • For α atomic, the case is immediate by substitution in Γ $ pt.uqn : βrb{asrb1 , and provided b ă 1, then b1 ă 1; • For α ” γ ˆ δ, there are independent terms xv, zyn such that, with possibly Γ ” ∆: Γ $ vn : γb , Γ, x : γb $ tn : βb1 and the base case applies; ∆ $ zn : δb , ∆, x : δb $ tn : βb1 and the base case applies; • For α ” γ ` δ, the term un is induced from un : γb˜2 and un : δb˜3 with b2 ` b4 ă 1; i.e., α is a metavariable for the distribution of possible outputs of the term u and also neither b2 “ 1 nor b3 “ 1. Then Γ, un : γb2 $ tn : βb̃ and Γ, un : δb3 $ tn : βb̃ , and for each the base case applies; • For α ” γ Ñ δ, the term un is of the form rxsvn : pγ Ñ δqrasrbă1 ; hence, x : γb2 $ vn : δb3 and y : pγ Ñ δqrbă1 $ tn : βrb1 allows to derive $ t.un : βrbă1srb1 ă1 . 5.1 Term Evaluation A term t : αa is said to probabilistically evaluate to a term t1 : αa1 1 if t can be transformed into t1 according to the rewriting rules in Figure 5. These term reduction rules correspond each to one typing rule from Figure 3 where some term transformation occur. Notably, they do not include rules where the term is not transformed and in particular the rules for ` which express the possible outputs of a given process. Note moreover that term transformation for expression including Ñ should be considered for their computational content, but do not affect output probability. Term reduction is abbreviated as tn ÞÑp t1n and ÞÑp˚ denotes its transitive and reflexive closure. Proposition 1. Given an aleathoric variable x : αa , the non-deterministic evaluation of atomic terms tn ÞÑp˚ t1n`m with output αã has as fix point the term whose output has probabilistic value a: tn ÞÑp˚ t1n`m ” limnÑ8 ã “ a. (1) Hence, by increasing the number of instances of the rule upd, we approximate better and better from ã the ideal value a of output α. The smaller this difference, the more trustworthy the process at hand. Proposition 2. If t ÞÑp˚ t1 • t : αa and t1 : αa1 with a1 ě a if and only ÞÑp˚ results from applying upd; • t : αa and t1 : βa1 with β Ă α and a1 ě a if and only if ÞÑp˚ results from applying E-ˆ. Hence, term evaluation of processes with an increasing output probability has to include at least as many instances of these rules such that the difference of ã from the probability a of the associated aleathoric variable in the appropriate distribution remains within the confidence interval or it reduces. 9 5.2 Safety A type safety result for TPTND expresses the fact that under trustworthiness conditions, the evaluation of a probabilistic process will lead to the intended output within allowed margins of certainty. This is shown by considering that any computation has bounded limits under which its output is probabilistically determined. This result is granted by preservation and progress. Theorem 3 (Output preservation). If Γ, x : αa $ tn : βb̃ and t ÞÑ˚p t1 according to the cases of Proposition 2, then Γ $ t1n : βb˜1 and b1 ě b. Proof. The proof is by induction on the term t and the appropriate reduction step which increases the probability of the output. Ñ – if tn has output β ” α, the only reduction step which applies is in the number n of executions of the rule upd which preserves α while increasing for t1 the value of b̃1 up to a. – if tn is a pair xt, uy with output pα ˆ βqc̃ , the reduction step corresponds to an instance of Eˆ from Γ, x : αa , y : βb $ t1n : αã (respectively t1n : βb̃ ), which increases for t1 the value of b̃1 compared to b̃. Hence, any of the above reduction steps preserves the output of the reduced term. Lemma 1. Γ, x : αa $ tn : βb̃ and t ÞÑ˚p t1 as by Theorem 3 if and only if Γ $ T rustpt1n : βb˜1 q. Proof. The left-to-right direction follows from Theorem 3 in that in each case the reduction step decreases the difference from the probability value of the corresponding aleathoric variable; the right-to-left direction follows from the conditions for the Trust operator. Ñ – If tn has output β ” α, | a ´ b˜1 |“ 0 for a sufficiently large number n, which satisfies the condition for T rustptn : βb̃ q. – If tn : pα ˆ βqc̃ and the reduction step leads to Γ, x : αa , y : βb $ t1n : αã (respectively t1n : βb̃ ) then ã ą c̃ (respectively b̃ ą c̃). Then the argument reduces to the base case; Ð – For the base case, if x : βb $ T rustpt1 : βb˜1 q, then by the IT rule | b ´ b1 |ď pnq. Hence the reduction x ÞÑp˚ t1 must have been applied so that (for n sufficiently big) | b ´ b1 |“ 0. – If Γ, x : αa , y : βb $ T rustpxt1 , u1 ym¨n : ppα ˆ βqã˚b̃ qq, then by the IT rule | pa ˚ bq ´ pã ˚ b̃q |ď pm ¨ nq. Hence there are reduction steps for Γ, x : αa $ t1m : αã and ∆, y : βb $ u1n : βb̃ , with t1 ‰ u1 such that for both the base case applies. Theorem 4 (Progress). If Γ, x : αb $ tn : αb̃ , then either it exists t1 such that t Ñp˚ t1 according to the reduction steps of Theorem 3 and Γ $ T rustpt1n`m : αb˜1 q, or tn is untrustworthy. Proof. Progress from tn to a trustworthy computation tn`m is guaranteed by Lemma 1 after a sufficiently large number of reduction steps which includes at least m new instances of the process t by the rule step upd (and possibly more, if t is not atomic). If any further reduction t Ñp˚ t1 corresponding to upd does not make b ´ b˜1 ď pn ` mq, we infer Γ $ T rustpt1n`m : αb˜1 q. The result generalizes for non-atomic terms in the case of reduction steps obtained by E-ˆ. Type safety for TPTND as obtained by preservation and progress tells us that any probabilistic computation can be evaluated in steps including experimental instances which increase its trustworthiness, intended as close- ness to the probability of its output as by the distribution under which it is formulated. Failing to reach such margin within the appropriate number of steps, determines an untrustworthy computation. Progress for TPTND does not require termination of the reduction process for the term tn , as usually required: this is due to the fact that the base case of such reduction corresponds to just a new sample extracted from a relevant distribution, and unless one assumes fixed resources, such execution is always possible. 10 6 Conclusion We have presented a type natural deduction system with terms decorated by a sample size and types by a probability value. The intended interpretation of judgements of the system TPTND is to assert the validity of the probabilistic output of a process, given a certain probability distribution. The main use of such a calculus is the determination of trustworthy probabilistic computations, expressed as the admissible distance from their theoretical probabilities. Such notion of trustworthiness can be used also to evaluate opaque distributions, e.g. in the context of Machine Learning systems, and it is guaranteed in TPTND by a safety result under specific conditions. Next steps of this work include: the development of a Coq verification protocol for probabilistic trustworthy computations, by extending the existing protocol for trust presented in [PB18] with one of the available Coq libraries for probabilistic reasoning, e.g. https://github.com/jtassarotti/polaris; the extension of TPTND with probabilistic intervals and imprecise probabilities; the use of TPTND in the verification of biased compu- tations. Another variation of TPTND can be foreseen which takes into account a finite number of resources, especially for experiments: in this format, safety can rely on a normal form for terms which is reached after a fixed number of possible experiments. Finally, TPTND falls within current investigations in uncertain reasoning and the development of sound relational and state transition semantics for this system are also planned. Acknowledgments This research was funded by the Department of Philosophy “Piero Martinetti” of the University of Milan under the Project "Departments of Excellence 2018-2022" awarded by the Ministry of Education, University and Research (MIUR). The authors also thankfully acknowledge the support of the Italian Ministry of Education, University and Research (PRIN 2017 project n. 20173YP4N3). Giuseppe Primiero acknowledges support of the NIAS- Lorentz Programme for funding the Interdisciplinary Theme Group on "Accountability in Medical Autonomous Expert Systems". References [Ald18] Alessandro Aldini. Design and verification of trusted collective adaptive systems. ACM Trans. Model. Comput. Simul., 28(2):9:1–9:27, 2018. [AT19] Alessandro Aldini and Mirko Tagliaferri. Logics to reason formally about trust computation and manipulation. In Andrea Saracino and Paolo Mori, editors, Emerging Technologies for Authorization and Authentication - Second International Workshop, ETAA 2019, Luxembourg City, Luxembourg, September 27, 2019, Proceedings, volume 11967 of Lecture Notes in Computer Science, pages 1–15. Springer, 2019. [Bor19] Marija Boričić. Sequent calculus for classical logic probabilized. Archive for Mathematical Logic, 58(1-2):119–136, 2019. [BPR15] Jaap Boender, Giuseppe Primiero, and Franco Raimondi. Minimizing transitive trust threats in software management systems. In Ali A. Ghorbani, Vicenç Torra, Hüseyin Hisil, Ali Miri, Ahmet Koltuksuz, Jie Zhang, Murat Sensoy, Joaquín García-Alfaro, and Ibrahim Zincir, editors, 13th Annual Conference on Privacy, Security and Trust, PST 2015, Izmir, Turkey, July 21-23, 2015, pages 191– 198. IEEE Computer Society, 2015. [CP19] Davide Ceolin and Giuseppe Primiero. A granular approach to source trustworthiness for negative trust assessment. In Weizhi Meng, Piotr Cofta, Christian Damsgaard Jensen, and Tyrone Grandison, editors, Trust Management XIII - 13th IFIP WG 11.11 International Conference, IFIPTM 2019, Copenhagen, Denmark, July 17-19, 2019, Proceedings, volume 563 of IFIP Advances in Information and Communication Technology, pages 108–121. Springer, 2019. [DBS17] Nagat Drawel, Jamal Bentahar, and Elhadi M. Shakshuki. Reasoning about trust and time in a system of agents. In Elhadi M. Shakshuki, editor, The 8th International Conference on Ambient Systems, Networks and Technologies (ANT 2017) / The 7th International Conference on Sustainable Energy Information Technology (SEIT 2017), 16-19 May 2017, Madeira, Portugal, volume 109 of Procedia Computer Science, pages 632–639. Elsevier, 2017. 11 [Dem04] Robert Demolombe. Reasoning about trust: A formal logical framework. In Christian Damsgaard Jensen, Stefan Poslad, and Theodosis Dimitrakos, editors, Trust Management, Second International Conference, iTrust 2004, Oxford, UK, March 29 - April 1, 2004, Proceedings, volume 2995 of Lecture Notes in Computer Science, pages 291–303. Springer, 2004. [DQBS20] Nagat Drawel, Hongyang Qu, Jamal Bentahar, and Elhadi M. Shakshuki. Specification and automatic verification of trust-based multi-agent systems. Future Gener. Comput. Syst., 107:1047–1060, 2020. [GIK` 18] Silvia Ghilezan, Jelena Ivetić, Simona Kašterović, Zoran Ognjanović, and Nenad Savić. Probabilistic reasoning about simply typed lambda terms. In International Symposium on Logical Foundations of Computer Science, pages 170–189. Springer, 2018. [HLHV10] Andreas Herzig, Emiliano Lorini, Jomi Fred Hübner, and Laurent Vercouter. A logic of trust and reputation. Log. J. IGPL, 18(1):214–244, 2010. [Lia03] Churn-Jung Liau. Belief, information acquisition, and trust in multi-agent systems–a modal logic formulation. Artif. Intell., 149(1):31–60, 2003. [LL17] Fenrong Liu and Emiliano Lorini. Reasoning about belief, evidence and trust in a multi-agent setting. In Bo An, Ana L. C. Bazzan, João Leite, Serena Villata, and Leendert W. N. van der Torre, editors, PRIMA 2017: Principles and Practice of Multi-Agent Systems - 20th International Conference, Nice, France, October 30 - November 3, 2017, Proceedings, volume 10621 of Lecture Notes in Computer Science, pages 71–89. Springer, 2017. [PB17] Giuseppe Primiero and Jaap Boender. Managing software uninstall with negative trust. In Jan-Philipp Steghöfer and Babak Esfandiari, editors, Trust Management XI - 11th IFIP WG 11.11 International Conference, IFIPTM 2017, Gothenburg, Sweden, June 12-16, 2017, Proceedings, volume 505 of IFIP Advances in Information and Communication Technology, pages 79–93. Springer, 2017. [PB18] Giuseppe Primiero and Jaap Boender. Negative trust for conflict resolution in software management. Web Intell., 16(4):251–271, 2018. [Pie20] A. D. Pierro. A type theory for probabilistic λ-calculus. In From Lambda Calculus to Cybersecurity Through Program Analysis, 2020. [PRCN17] Giuseppe Primiero, Franco Raimondi, Taolue Chen, and Rajagopal Nagarajan. A proof-theoretic trust and reputation model for VANET. In 2017 IEEE European Symposium on Security and Privacy Workshops, EuroS&P Workshops 2017, Paris, France, April 26-28, 2017, pages 146–152. IEEE, 2017. [Pri20] Giuseppe Primiero. A logic of negative trust. J. Appl. Non Class. Logics, 30(3):193–222, 2020. [Sin11] Munindar P. Singh. Trust as dependence: a logical approach. In Liz Sonenberg, Peter Stone, Ka- gan Tumer, and Pinar Yolum, editors, 10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2011), Taipei, Taiwan, May 2-6, 2011, Volume 1-3, pages 863–870. IFAAMAS, 2011. [WF94] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, 1994. 12