阿日哥的向量空间

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 ...

de Bruijn Notation One way to avoid the tricky interaction between free and bound names in the substitution operator is to pick a representation for expressions that doesn’t have any names at all! Intuitively, we can think of a bound variable is just a pointer to the that binds it. For example, in , the points to the first and the points to the second . So-called de Bruijn notation uses this idea as the representation for expressions. Here is the grammar for expressions in de Bruijn notation: ...

Nontermination Consider the expression , which we will refer to as for brevity. Let’s try evaluating : Evaluating never reaches a value! It is an infinite loop! What happens if we use as an actual argument to a function? Consider this program: If we use CBV semantics to evaluate the program, we must reduce to a value before we can apply the function. But never evaluates to a value, so we can never apply the function. Thus, under CBV semantics, this program does not terminate. If we use CB ...

Lambda Calculus Encodings Booleans The pure -calculus contains only functions as values. It is not exactly easy to write large or interesting programs in the pure -calculus. We can however encode objects, such as booleans, and integers. Let us start by encoding constants and operators for booleans. That is, we want to define functions TRUE, FALSE, AND, NOT, IF, and other operators that behave as expected. For example: Let’s start by defining TRUE and FALSE: Thus, both TRUE and FALSE are functi ...

Lambda Calculus Evaluation There are many different evaluation strategies for the -calculus. The most permissive is full reduction, which allows any redex--i.e., any expression of the form --to step to at any time. It is defined formally by the following small-step operational semantics rules: The call by value (CBV) strategy enforces a more restrictive strategy: it only allows an application to reduce after its argument has been reduced to a value (i.e., a -abstraction) and does not allow ev ...

Lambda calculus (or -calculus) was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s to describe functions in an unambiguous and compact manner. Many real languages are based on the lambda calculus, including Lisp, Scheme, Haskell, and ML. A key characteristic of these languages is that functions are values, just like integers and booleans are values: functions can be used as arguments to functions, and can be returned from functions. The name “lambda calculus” comes from the use ...

Relative Completeness Previously, we discussed the issue of completeness—i.e., whether it is possible to derive every valid partial correctness specification using the axioms and rules of Hoare logic. Unfortunately, if treated as a pure deductive system, Hoare logic cannot be complete. To see why, consider the following partial correctness specifications: The first is valid if and only if the assertion is valid while the second is valid if and only if the command does not halt. It turns out t ...

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 ...