阿日哥的向量空间

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

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

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