daig

// https://blogs.oracle.com/linux/post/hello-from-a-libc-free-world-part-1
// entry code for compiling with `-nostdlib` :
// `gcc -nostdlib -c -fno-no-stack-protector -fno-exceptions -fno-asynchronous-unwind-tables hello.c` // compile without linking
// `gcc -nostdlib -c stubstart.S` // compile the entry code
// `ld stubstart.o hello.o -o hello` // link the entry code and the compiled code
.global _start //global entry point for the program.
_start: call main //enter the main function
        movl $1, %eax // put 1, the syscall number for SYS_exit
        xorl %ebx, %ebx // put 0, the exit code for success (argument to SYS_exit)
        int $0x80 // call the kernel interrupt to exit

daig

#sudo apt install inotify-tools
inotifywait -m --format "%w%f" -e modify ./ --include *.cpp |
while read changed; do
      echo $changed
      g++ -std=c++20 $changed && ./a.out;
done

daig

#include <iostream>
#include <vector>
#include <variant>
#include <string>

using namespace std;

template<typename ... Ts>
struct cases : Ts ... {using Ts::operator() ...; };
template<class... Ts> cases(Ts...) -> cases<Ts...>;

daig

Logical Inductors as Proof Search

Logical Inductors rely on a robust interplay between markets and individual traders betting on the eventual output of logical computations, to develop accurate beliefs identifying features long ahead of a standard deductive process. Interestingly, inductors also identify constraints-between / properties-about logical variables (ex: “is the asymptotic distribution of primes n/log(n)?”) before concrete statements (ex: ”is this particular large X prime?”). This decomposition of a difficult statement into the total of (entropically) smaller properties is reminiscent of a yoneda embedding. This is in stark contrast with most proof search, which works towards (or backwards from) a specific goal proposition.

Meanwhile, polarized linear logic has a family of proof-net-search methods operating dually on both potentially-provable propositions and potentially-refutable properties. Such methods describe a concurrent deductive phase analogous to indiv

daig

Epistemic Status Highly speculative. I speak informally whenever possible but use technical terms to point when no such common language is satisfactory. This isn't meant to imply certainty or prescriptiveness - The intention here is to gesture at something powerful with the rhetorical tools I have available. For brevity I factor out uncertainty to this warning, and present all conjecture as fact, so insert "I suspect" before everything that sounds like an assertion.

TL;DR A rough account for the meaning of reflection in multilevel inductors

Motivation

The reference "implementation" for logical induction has two components

daig

/* gcc -dM -E - < /dev/null */


#define __SSP_STRONG__ 3
#define __DBL_MIN_EXP__ (-1021)
#define __UINT_LEAST16_MAX__ 0xffff
#define __ATOMIC_ACQUIRE 2
#define __FLT128_MAX_10_EXP__ 4932
#define __FLT_MIN__ 1.17549435082228750796873653722224568e-38F
#define __GCC_IEC_559_COMPLEX 2

daig

set nocompatible
set number
set ruler
set nowrap
set showmode
set tw=80
set smartcase
set smarttab
set smartindent

daig

\newcommand{\chumorph}[5]{
\color{mgrey}
\[
\begin{tikzcd}[ampersand replacement=\&]
\& \chuneu{#1} \& \\
\chupos{#4^+} \ar[rr, "\chupos{#2^+}"] \ar[rd, harpoon, bend right=38] \ar[dd, shift left=0.7, no head, "\chuneu{\overline{#4}}"] \& \& \chupos{#5^+} \ar[dd,phantom, shift left=1.5, "\times"] \ar[ld, harpoon', bend left=38] \\
 \& \chuneu{#3} \& \\
\chuneg{#4^-} \ar[uu, phantom, shift left=1.5, "\times"] \ar[ur, harpoon', bend left=38] \& \& \chuneg{#5^-} \ar[uu, no head, shift left=0.7, "\chuneu{\overline{#5}}"] \ar[lu, harpoon, bend right=38] \ar[ll, "\chuneg{#2^-}"]
\end{tikzcd}
\]

daig

% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------

\ProvidesPackage{agda}

\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
                calc, environ, xparse, xkeyval}

% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation

daig

{-# OPTIONS --type-in-type #-}
module functors where
open import prelude

record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where
  constructor 𝒾:_▸:_𝒾▸:_▸𝒾:
  infixl 8 _▸_
  field
    𝒾 : ∀ {x} → 𝒞[ x , x ]
    _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ]