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

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


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

	/* 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

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

	#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

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