Hirrolot

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by the program; let us call this machine M₁. In observing the operation of

suhr

Как рассуждать в программировании (ссылки)

База — формальные доказательства:

• https://leanprover.github.io/logic_and_proof/
• https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

База — математика:

• «Конкретная математика. Основание информатики» (Д. Кнут)

Hirrolot

type cps_var =
  (* Taken from the lambda term during CPS conversion. *)
  | CLamVar of string
  (* Generated uniquely during CPS conversion. *)
  | CGenVar of int

type cps_term =
  | CFix of (cps_var * cps_var list * cps_term) list * cps_term
  | CAppl of cps_var * cps_var list
  | CRecord of cps_var list * binder

Hirrolot

(* A variable identifier of the lambda language [term]. *)
type var = string [@@deriving eq]

(* The lambda language; direct style. *)
type term =
  | Var of var
  | Fix of (var * var list * term) list * term
  | Appl of term * term list
  | Record of term list
  | Select of term * int

Hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

Hirrolot

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

suhr

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.

martinchapman

# Visualise a latex document git history

# loop through commits, create a PDF from your main file for each
# translate the pages of that PDF to a single image
# create GIF/mp4 from the folder of images created

# run within your local repository
# prerequisites: ImageMagick and FFmpeg

# create output folder

raysan5

CUSTOM GAME ENGINES: A Small Study

A couple of weeks ago I played (and finished) A Plague Tale, a game by Asobo Studio. I was really captivated by the game, not only by the beautiful graphics but also by the story and the locations in the game. I decided to investigate a bit about the game tech and I was surprised to see it was developed with a custom engine by a relatively small studio. I know there are some companies using custom engines but it's very difficult to find a detailed market study with that kind of information curated and updated. So this article.

Nowadays lots of companies choose engines like Unreal or Unity for their games (or that's what lot of people think) because d

pedrominicz

The originality of these Gists varies drastically. Most are inspired by the work of others, in that case, all merit goes to the original authors. I have linked everything used as reference material on the Gists themselves.

Haskell

• Crégut's strongly reducing Krivine abstract machine
• Type-check STLC into a GADT
• Alex: indentation-sensitive lexer
• A-normalization (administrative normal form, ANF)
• Number of SK-combinator calculus terms of a given size
• Number of untyped lambda calculus terms of a given size