分布式系统入门：保罗·西维洛蒂的讲解

分布式系统

需积分: 9 63 浏览量更新于2024-07-23 收藏 741KB PDF 举报

身份认证购VIP最低享 7 折!

30元优惠券

资源详情

资源推荐

4 CHAPTER 1. BOOLEANS, PREDICATES, AND QUANTIFICATION

and obvious. Nevertheless, this distinction quickly b ecomes blurred when we

consider operations. The familiar operations on booleans (e.g., ∧ , ∨ ) can

also be applied to predicates! They are technically diﬀerent operations, since

they have diﬀerent signatures, but confusion can arise because the same symbol

is usually used.

∧ : boolean × boolean → boolean

∧ : predicate × predicate →

Typically, the operator being used is clear from context (i.e., from the types

of the arguments). We could add subscripts to distinguish these operators, but

this would needlessly clutter our expressions and mask many of the common-

alities between these diﬀerent versions of fundamentally similar functions (with

fundamentally similar properties).

For example, consider the predicates is tall and is heavy . The expression

is tall ∧ is heavy denotes a predicate! It is therefore a function that can be

applied to particular elements of its domain, for example:

(is tall ∧ is heavy).Jeff

This results in a boolean. See Figure 1.2 for a graphical representation.

is_tallis_heavy

Sindhu

Jeff

Mikko

Figure 1.2: The Conjunction of Two Predicates

In this way, a simple operator on boolean ( ∧ ) has been elevated to operate

on functions that map to boolean. This overloading of a single symbol is called

lifting. Of course, the process of lifting can continue, elevating the operator to

apply to functions that map to functions that map to boolean. And so on.

Lifting can be applied to the constants true and false as well. These symbols

have been introduced as the elements of the set of boolean. But they can also be

lifted to be predicates (the former mapping to true everywhere, and the latter

to false). This leads us into the topic of what is meant by “everywhere”...

1.2.4 Everywhere Brackets

Consider the following expression:

is tall ≡ is heavy

8 CHAPTER 1. BOOLEANS, PREDICATES, AND QUANTIFICATION

1.3.3 Proof Format

The axioms above give the basic properties of our operators. They can be used

to derive further properties of these operators as theorems. A theorem must be

proven from a set of axioms and theorems that have already been proven. To

carry out these proofs, we will use a precise notation. This notation will help us

structure our proofs so they are easy to read and verify. Perhaps surprisingly,

this format also frequently makes proofs easier to write since it will often suggest

the next step to be carried out.

Proofs are carried out in a calculational style. Each step in the proof involves

the application of one (or more) axioms or theorems. Each step is annotated

with a hint for the reader justifying that step. Each step should be small enough

that a reader can be easily convinced the step is correct. Beware of steps that

involve the application of multiple axioms or theorems! These steps are often

where trouble arises. As you write proofs, you will develop a feel for the appro-

priate granularity of these steps: Too small and the proof is pedantic and hard

to follow, but too large and the pro of is obscure and hard to follow. Some ax-

ioms are used so ubiquitously they are frequently omitted (e.g., commutativity

of ≡ and of ∨ ). As a rule of thumb, error on the side of thoroughness.

As an general example of our calculational pro of notation, consider a proof

of [A ≡ B] . One such proof might take the form:

≡ { reason why [A ≡ C] }

≡ { reason why [C ≡ B] }

A (less nice) alternative for such a proof would be:

A ≡ B

≡ { reason why [A ≡ B ≡ D] }

≡ { reason why [D ≡ true] }

true

Writing proofs in this way will give us a common structure in which to read

each other’s proofs. It will also encourage a nice discipline of justifying steps in a

precise manner. Notice, also, that expressions written in this format have a very

diﬀerent meaning than their straight-line counterparts. That is, the meaning of

≡

剩余153页未读，继续阅读

williamshyy

粉丝: 0
资源: 1

分布式系统入门：保罗·西维洛蒂的讲解

Introduction to Distributed Systems

[Google] Introduction to Distributed System Design.pdf

Distributed Systems 分布式系统基础架构

Scaling Distributed Systems in ARCO Design Environments

distributed systems: concepts and design 第五版知识点概括

.net orleans

distributed systems--principle and paradigms

distributed systems – principles and paradigms课后答案

ZooKeeper in programing

distributed systems

george c,jean d tim k,et al.distributed systems:concepts and design[eb/ol]

distributed systems 3rd

Com.alibaba.dubbo.remoting

多智能体强化学习推荐书籍

帮我检索20篇有关语义协同的外文文献

Spring cloud

Apache Mesos frameworks

1、简述如何配置nacos注册发现中心

TimeDistributed is not defined

Time distributed layer

最新资源