阿日哥的向量空间

Here are some useful courses and learning materials. HPC MIT 6.172 Performance Engineering of Software Systems, Fall 2018 UCB CS267 Spring 2023 - Application of Parallel Computers CS121-Parallel Computing Machine Learning 国立台湾大学 李宏毅 机器学习 Deep Learning Systems Course Book - 机器学习中的概率统计 Machine Learning System CMU 10-414/714: Deep Learning Systems Machine Learning Compilation Compiler & Program Analysis Cornell CS 4120 Introduction of Compilers Cornell CS 6120: Advanced Compilers: The Self-Guid ...

Decorated Programs Doing a complete proof in Hoare Logic can feel overly verbose. The “core” of a proof consists of the preconditions and postconditions surrounding every command; with those, it’s usually possible to infer the complete shape of the proof tree. Decorating programs is a way to informally write down a Hoare logic proof of correctness. The idea is to insert assertion decorations between every “line” of the program. Using this informal evidence, you can reconstruct the full formal pr ...

Hoare Logic How do we show that a partial correctness statement с holds? We know that с is valid if it holds for all stores and interpretations: с. Furthermore, showing that с requires reasoning about the execution of command (that is, ), as indicated by the definition of validity. It turns out that there is an elegant way of deriving valid partial correctness statements, without having to reason about stores, interpretations, and the execution of . We can use a set of inference rules and axiom ...

Introduction to Axiomatic Semantics Now we turn to the third and final main style of semantics, axiomatic semantics. The idea in axiomatic semantics is to define meaning in terms of logical specifications that programs satisfy. This is in contrast to operational models (which show how programs execute) and denotational models (which show what programs compute). This approach to reasoning about programs and expressing program semantics was originally proposed by Floyd and Hoare and was developed ...

Last time we defined the denotational semantics of IMP: In this lecture we’ll prove Kleene’s fixpoint theorem, which shows that the fixed point used to define the semantics of while commands exists, and work through examples of reasoning using the denotational semantics. Kleene’s Fixpoint Theorem Definition (Scott Continuity). A function from to is said to be Scott-continuous if for every chain we have It is not hard to show that if is Scott continuous, then it is also monotonic—that is, ...

We have now seen two operational models for programming languages: small-step and large-step. In this nnote, we consider a different semantic model, called denotational semantics. The idea in denotational semantics is to express the meaning of a program as the mathematical function that expresses what the program computes. We can think of an IMP program as a function from stores to stores: given an an initial store, the program produces a final store. For example, the program can be thought of ...

Equivalence of Semantics The small-step and large-step semantics are equivalent as captured by the following theorem. Theorem. For all commands and stores and we have The proof is left as an exercise. Non-Termination For a given command and initial state , the execution of the command may terminate with some final store , or it may diverge and never yield a final state. For example, the command always diverges while diverges if and only if the value of variable in the initial state is po ...

A Simple Imperative Language We will now consider a more realistic programming language, one where we can assign values to variables and execute control constructs such as if and while. The syntax for this imperative language, called IMP, is as follows: Small-step Operational Semantics We’ll first give a small-step operational semantics for IMP. The configurations in this language are of the form , , and , where is a store. The final configurations are of the form for commands, and for Bool ...

Large-Step Operational Semantics In the last lecture we defined a semantics for our language of arithmetic expressions using a small-step evaluation relation (and its reflexive and transitive closure ). In this note we will explore an alternative approach--large-step operational semantics--which yields the final result of evaluating an expression directly. Defining a large-step semantics boils down to specifying a relation that captures the evaluation of an expression. The relation has the fo ...

In this note, we will use the semantics of our simple language of arithmetic expressions, to express useful program properties, and we will prove these properties by induction. Program Properties There are a number of interesting questions about a language one can ask: Is it deterministic? Are there non-terminating programs? What sorts of errors can arise during evaluation? Having a formal semantics allows us to express these properties precisely. Determinism: Evaluation is deterministic, T ...