VictorTaelin

Y = λf (f (Y f))

(App n) = match n {
  0: λf λx x
  +: λf λx (App (/ n 2) λx(f (f x)) (match m = (% n 2) { 0: x; +: (f x) }))
}

B0 = λb0 λb1 b0
B1 = λb0 λb1 b1

VictorTaelin

Brief history of Type Theory - Human Timeline

All started around 1930, when mathematicians discovered the λ-calculus. It was Turing complete, so we wrote programs on it. Everything was great, until the first program crashed and the first paradox was found. The world was in flames, so humans looked for better.

Around 1940, the simple type was discovered. It solved everything: math was consistent again, programs stopped crashing. People were happy, until someone tried to make a linked list.

"Why do I need to duplicate my entire codebase?" - asked the angry developers.

At this point, half of humanity gave up on types. A duck religion was born. The other half looked for better.

VictorTaelin

// Interaction Calculus of Constructions
// =====================================

// Type
// ----

data Term
  = (Lam bod)
  | (App fun arg)
  | (Val bod)

VictorTaelin

// In this file, I explored the idea of computing the solution of:
// (3^x) % (2^s) == 1
// By using superpositions. The approach I used is to create an hand-optimized
// Mul3 function that seems to be efficient, and then creating a superposition
// of all Church Nats, as a perfect binary tree in the shape {{{0 1} {2 3}}...},
// and then applying that to `mul3` of `1`. As a result, we'll have a sup of all
// multiples of 3 (as binary strings). We can then call the function "Is1" on
// that sup. The result is a big superpositions of `0`, except for the places
// where we have a solution for the equation, which are `1`. This algorithm,
// despite all involved functions fusing, is exponential. After thinking about

VictorTaelin

// COMPUTATION RULES
// ===================================================
// APP | ((λx body) arg)
//  X  | ---------------------------------------------
// LAM | x ~ arg; body
// ===================================================
// APP | ({fst snd} arg)
//  X  | ---------------------------------------------
// SUP | dup #L{a,b} = arg; {(fst a) (snd b)}
// ===================================================

VictorTaelin

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

VictorTaelin

// THOUGHTS
//
// Consider FP: ∃f ∀a ∀b (f (mul a b) b) == b
//
// FP can be proven with a pair:
//
// - F: (a b: Nat) -> Nat
// - P: (a b: Nat) -> (F (mul a b) b) == b
//
// In the proof P, we pattern-match on 'a' and 'b'. Note that EVERY equality can

VictorTaelin

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. A more complete file, including
// superpositions (for optimal unification) is available on the
// Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.

VictorTaelin

study: https://link.springer.com/article/10.1007/s11357-023-00980-6

Q: What are the main findings of the article above?

A: The main findings of the article are that a plasma fraction treatment derived from young adult pigs, termed E5, significantly reversed aging in rats according to epigenetic clocks and other biomarkers of aging. The treatment more than halved the epigenetic ages of blood, heart, and liver tissue, and also showed a significant rejuvenation effect in the hypothalamus. Alongside this, the treatment led to improvements in organ function, reduced markers of chronic inflammation and oxidative stress, increased antioxidant levels, and improved cognitive functions in the rats. The study also developed six different epigenetic clocks for rat tissues, two of which can be applied to humans as well.

Q: How clinically significant were the objective improvements observed? Provide an extensive list of measured markers and effect size.

A: The objective improvements observed in the study were clinicall

VictorTaelin

ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

JS

const Lam = bod => lam => app => vah => lam(bod);
const App = fun => arg => lam => app => vah => app(fun)(arg);
const Var = exp => lam => app => vah => vah(exp);

const nz = v => nz => ns => nz(v);