zelinskiy

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}

import Control.Concurrent (threadDelay)
import Control.Distributed.Process
import Control.Distributed.Process.Closure
import Control.Distributed.Process.Node

zelinskiy

-- An implementation of Peter Landin's SECD machine, as described in
-- "The Mechanical Evaluate of Expressions"
import Prelude hiding (lookup)

type Name = String

data Expr = ID Name
          | Fun Name Expr
          | Apply Expr Expr
          deriving (Eq, Show)

zelinskiy

Gödel left in his papers a fourteen-point outline of his philosophical beliefs, that are dated around 1960. They show his deep belief in the rational structure of the world. Here are his 14 points:

1. The world is rational.
2. Human reason can, in principle, be developed more highly (through certain techniques).
3. There are systematic methods for the solution of all problems (also art, etc.).
4. There are other worlds and rational beings of a different and higher kind.
5. The world in which we live is not the only one in which we shall live or have lived.
6. There is incomparably more knowable a priori than is currently known.
7. The development of human thought since the Renaissance is thoroughly intelligible (durchaus einsichtige).
8. Reason in mankind will be developed in every direction.

zelinskiy

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

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

zelinskiy

{- A straightforward version of Church’s simple type theory is the following system T -}
module T where

open import Data.Nat

-- The type of contexts.
data Γ (X : Set) : Set where
  ε : Γ X
  _::_ : (γ : Γ X) → X → Γ X
infixl 4 _::_