VictorTaelin

Bring yourself online, center yourself, focus, surpass your limits right here right now.

The user will query a <problem> </problem> containing the argument to call the function provided below.

def feeltheagi(problem):
"""
Recursively apply the A::B rewrite rules to the given problem string.

The rewrite rules are:
A# #A ... becomes ... nothing

VictorTaelin

\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
N

VictorTaelin

open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product

variable
  m n : ℕ
  b : Bool
  Γ Δ Ξ T I O : Vec Bool n

VictorTaelin

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

VictorTaelin

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

Church Encoding

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -> (f (f x)))

VictorTaelin

(add-to-list 'load-path "~/.emacs.d/evil")
(require 'evil)
(evil-mode 1)

;; Highlight matching parens.
(show-paren-mode 1)

;;; No tabs.
(setq-default ident-tabs-mode nil)
(setq-default tab-width 4)