Skip to content

Instantly share code, notes, and snippets.

@yumura
Last active May 11, 2020 15:33
Show Gist options
  • Save yumura/d22146f63fea915391e090205810ccdf to your computer and use it in GitHub Desktop.
Save yumura/d22146f63fea915391e090205810ccdf to your computer and use it in GitHub Desktop.
Lambda calculus :: PowerShell
New-Variable LambdaAbstractionSeparater '.' -Option Constant
filter New-Lambda
{
switch ($args.Count)
{
0 {
throw "New-Lambda : 空列は解析できません。"
}
1 {
return NewLambda1 $args 0
}
2 {
return New-LambdaApplication `
(NewLambda1 $args 0) `
(NewLambda1 $args 1)
}
}
# {$xs.Count -ge 3} is True
$sepIndex = @(
for ($i = 0; $i -lt $args.Count; $i++)
{if ($args[$i] -eq $LambdaAbstractionSeparater)
{$i}})
switch ($sepIndex.Count)
{
0 {
$term = NewLambda1 $args 0
for ($i = 1; $i -lt $args.Count; $i++)
{$term = New-LambdaApplication $term (NewLambda1 $args $i)}
return $term
}
1 {
switch ($sepIndex[0])
{
0 {
throw "New-Lambda : 区切文字が先頭にあります。項番:${_}。"
}
($args.Count - 1) {
throw "New-Lambda : 区切文字が末尾にあります。項番:${_}。"
}
default {
$term = NewLambda1 $args ($sepIndex[0] + 1)
for ($i = $sepIndex[0] + 2; $i -lt $args.Count; $i++)
{$term = New-LambdaApplication $term (NewLambda1 $args $i)}
for ($i = $sepIndex[0] - 1; $i -ge 0; $i--)
{
$var = NewLambda1 $args $i
if ($var.PSTypeNames[0] -eq "Lambda.Variable")
{
$term = New-LambdaAbstraction $var $term
}
else
{
throw "New-Lambda : 区切文字より左に変数でないラムダ式があります。項番:${i}"
}
}
return $term
}
}
}
default {
throw "New-Lambda : 区切文字が多すぎます。項番 : $($sepIndex -join ", ")。"
}
}
}
filter NewLambda1 ([array]$Array, [int]$Index)
{
switch (,$Array[$Index])
{
{$_ -is [string] -and $_ -ne $LambdaAbstractionSeparater} {
return New-LambdaVariable $_
}
{Test-Lambda $_} {
return $_
}
default {
throw "New-Lambda : 解析できない要素です。項番:${Index}。"
}
}
}
filter Test-Lambda ($InputObject)
{$InputObject -is [PSObject] -and $InputObject.PSTypeNames[1] -eq "Lambda"}
filter New-LambdaVariable
{
Param
(
[Parameter(Mandatory=$true)]
[String] $Name
)
if ($Name -eq $LambdaAbstractionSeparater)
{throw "New-LambdaVariable : 変数名に区切文字は使用できません。"}
New-Module -AsCustomObject -ArgumentList $Name {
Param (${#Name})
New-Variable Name ${#Name} -Option Constant
filter ToString() {Get-LambdaString $this}
Export-ModuleMember `
-Function ToString `
-Variable Name
} |
Add-Member -TypeName "Lambda" -PassThru |
Add-Member -TypeName "Lambda.Variable" -PassThru
}
filter New-LambdaApplication
{
Param
(
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $Function,
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $Term
)
New-Module -AsCustomObject -ArgumentList $Function, $Term {
Param (${#Function}, ${#Term})
New-Variable Function ${#Function} -Option Constant
New-Variable Term ${#Term} -Option Constant
filter ToString() {Get-LambdaString $this}
Export-ModuleMember `
-Function ToString `
-Variable Function, Term
} |
Add-Member -TypeName "Lambda" -PassThru |
Add-Member -TypeName "Lambda.Application" -PassThru
}
filter New-LambdaAbstraction
{
Param
(
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda.Variable")] $Variable,
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $Term
)
New-Module -AsCustomObject -ArgumentList $Variable, $Term {
Param (${#Variable}, ${#Term})
New-Variable Variable ${#Variable} -Option Constant
New-Variable Term ${#Term} -Option Constant
filter ToString() {Get-LambdaString $this}
Export-ModuleMember `
-Function ToString `
-Variable Variable, Term
} |
Add-Member -TypeName "Lambda" -PassThru |
Add-Member -TypeName "Lambda.Abstraction" -PassThru
}
filter Get-LambdaString
{
Param
(
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
switch ($Lambda.PSTypeNames[0])
{
Lambda.Variable {
return "\ " + $Lambda.Name
}
Lambda.Application {
filter format ([PSTypeName("Lambda")] $term)
{
switch ($term.PSTypeNames[0])
{
Lambda.Variable {
return $term.Name
}
Lambda.Application {
$str = Get-LambdaString $term
return "(${str})"
}
Lambda.Abstraction {
$str = Get-LambdaString $term
return "(${str})"
}
default {throw $term}
}
}
$stack = New-Object "System.Collections.Generic.Stack[String]"
$func = $Lambda
while ($func.PSTypeNames[0] -eq "Lambda.Application")
{
$stack.Push((format $func.Term))
$func = $func.Function
}
$stack.Push((format $func))
"\ " + ($stack -join " ")
}
Lambda.Abstraction {
$var = New-Object "System.Collections.Generic.List[String]"
$term = $Lambda
while ($term.PSTypeNames[0] -eq "Lambda.Abstraction")
{
[void] $var.Add($term.Variable.Name)
$term = $term.Term
}
$term = Get-LambdaString $term
$term = $term.Substring(2, $term.Length - 2)
return "\ $($var -join " ") . ${term}"
}
default {throw}
}
}
filter Get-LambdaVariable
{
Param
(
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda,
[switch] $Free,
[switch] $Bind
)
$type = switch ($true)
{
{$Free -and -not $Bind} {"Free"}
{-not $Free -and $Bind} {"Bind"}
Default {"Default"}
}
$var = New-Object "System.Collections.Generic.HashSet[String]"
GetLambdaVariable $Lambda $type $var
,$var
}
filter GetLambdaVariable
{
Param
(
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $Lambda,
[string] $Type,
[ValidateNotNull()]
[System.Collections.Generic.HashSet[String]]
$Variable
)
switch ($Lambda.PSTypeNames[0])
{
Lambda.Variable {
if ($Type -eq "Bind")
{return}
[void]$Variable.Add($Lambda.Name)
}
Lambda.Application {
GetLambdaVariable $Lambda.Function $Type $Variable
GetLambdaVariable $Lambda.Term $Type $Variable
return
}
Lambda.Abstraction {
if ($Type -eq "Free")
{
$var = New-Object "System.Collections.Generic.HashSet[String]"
GetLambdaVariable $Lambda.Term $Type $var
[void]$var.Remove($Lambda.Variable.Name)
$Variable.UnionWith($var)
}
else
{
[void]$Variable.Add($Lambda.Variable.Name)
GetLambdaVariable $Lambda.Term $Type $Variable
}
return
}
default {throw}
}
}
filter Convert-LambdaAlpha
{
Param
(
[Parameter(Mandatory=$true)]
[int] $Index,
[Parameter(Mandatory=$true)]
[string] $After,
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
if ($Index -lt 0)
{return $Lambda}
$i = $Index + 1
$i, $c, $l = ConvertLambdaAlpha $i "" $After $Lambda
$l
}
filter ConvertLambdaAlpha
{
Param
(
[Parameter(Mandatory=$true)]
[Int] $Index,
[ValidateNotNull()]
[string] $Before,
[Parameter(Mandatory=$true)]
[string] $After,
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
if ($Index -lt 0)
{return $Index, $false, $Lambda}
switch ($Lambda.PSTypeNames[0])
{
Lambda.Variable {
if ($Index -gt 0 -or $Lambda.Name -ne $Before)
{return $Index, $false, $Lambda}
return $Index, $true, (New-LambdaVariable $After)
}
Lambda.Application {
$Index, $changeFunc, $func = ConvertLambdaAlpha $Index $Before $After $Lambda.Function
$Index, $changeTerm, $term = ConvertLambdaAlpha $Index $Before $After $Lambda.Term
if ($changeFunc -or $changeTerm)
{return $Index, $true, (New-LambdaApplication $func $term)}
return $Index, $false, $Lambda
}
Lambda.Abstraction {
switch ($Index)
{
0 {
switch ($Lambda.Variable.Name)
{
$Before {
return $Index, $false, $Lambda
}
$After {
$fv = Get-LambdaVariable $Lambda -Free
if ($fv.Contains($Before))
{throw "Convert-LambdaAlpha : After(${After})が新たに束縛されてしまうため変換できません。"}
return $Index, $false, $Lambda
}
default {
$Index, $changeTerm, $term = ConvertLambdaAlpha $Index $Before $After $Lambda.Term
if ($changeTerm)
{return $Index, $true, (New-LambdaAbstraction $Lambda.Variable $term)}
return $Index, $false, $Lambda
}
}
}
1 {
$fv = Get-LambdaVariable $Lambda -Free
if ($fv.Contains($After))
{throw "Convert-LambdaAlpha : After(${After})が既に存在する自由変数と重複するため変換できません。"}
$Index, $changeTerm, $term = ConvertLambdaAlpha 0 $Lambda.Variable.Name $After $Lambda.Term
return -1, $true, (New-LambdaAbstraction (New-LambdaVariable $After) $term)
}
default
{
$Index--
$Index, $changeTerm, $term = ConvertLambdaAlpha $Index $Before $After $Lambda.Term
if ($changeTerm)
{return $Index, $true, (New-LambdaAbstraction $Lambda.Variable $term)}
return $Index, $false, $Lambda
}
}
}
default {throw}
}
}
filter Convert-LambdaSubstitution
{
Param
(
[Parameter(Mandatory=$true)]
[string] $Before,
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $After,
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
if ($After.PSTypeNames[0] -eq "Lambda.Variable" -and $After.Name -eq $Before)
{return $Lambda}
$c, $l = ConvertLambdaSubstitution @PSBoundParameters (Get-LambdaVariable $After -Free)
$l
}
filter ConvertLambdaSubstitution
{
Param
(
[Parameter(Mandatory=$true)]
[string] $Before,
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $After,
[Parameter(Mandatory=$true)]
[PSTypeName("Lambda")] $Lambda,
[ValidateNotNull()]
[System.Collections.Generic.HashSet[String]]$FreeVariable
)
switch ($Lambda.PSTypeNames[0])
{
Lambda.Variable {
if ($Lambda.Name -eq $Before)
{return $true, $After}
return $false, $Lambda
}
Lambda.Application {
$changeFunc, $func = ConvertLambdaSubstitution $Before $After $Lambda.Function $FreeVariable
$changeTerm, $term = ConvertLambdaSubstitution $Before $After $Lambda.Term $FreeVariable
if ($changeFunc -or $changeTerm)
{return $true, (New-LambdaApplication $func $term)}
return $false, $Lambda
}
Lambda.Abstraction {
if ($Lambda.Variable.Name -eq $Before)
{return $false, $Lambda}
if (-not $FreeVariable.Contains($Lambda.Variable.Name))
{
$change, $term = ConvertLambdaSubstitution $Before $After $Lambda.Term $FreeVariable
if ($change)
{return $true, (New-LambdaAbstraction $Lambda.Variable $term)}
return $false, $Lambda
}
$var = Get-LambdaVariable $Lambda.Term
if (-not $var.Contains($Before))
{return $false, $Lambda}
$max = $var + $FreeVariable |
Where-Object {$_ -match "_\d+"} |
Sort-Object -Descending |
Select-Object -First 1
$newName =
if ($null -eq $max) {"_0"}
else {
$head = $max.Substring(0, $max.length - 1)
$tail = [string]([int]::Parse($max[-1]) + 1)
$head + $tail
}
$newL = $Lambda | Convert-LambdaAlpha 0 $newName
$c, $newTerm = ConvertLambdaSubstitution $Before $After $newL.Term $FreeVariable
return $true, (New-LambdaAbstraction $newL.Variable $newTerm)
}
default {throw}
}
}
filter Convert-LambdaBeta
{
Param
(
[Parameter(Mandatory=$true)]
[int] $Index,
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
if ($Index -lt 0)
{return $Lambda}
$i = $Index + 1
$i, $c, $l = ConvertLambdaBeta $i $Lambda
$l
}
filter ConvertLambdaBeta
{
Param
(
[Parameter(Mandatory=$true)]
[int] $Index,
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda
)
if ($Index -lt 0)
{return $Index, $false, $Lambda}
switch ($Lambda.PSTypeNames[0])
{
Lambda.Variable {
return $Index, $false, $Lambda
}
Lambda.Application {
if ($Lambda.Function.PSTypeNames[0] -ne "Lambda.Abstraction")
{
$Index, $changeFunc, $func = ConvertLambdaBeta $Index $Lambda.Function
$Index, $changeTerm, $term = ConvertLambdaBeta $Index $Lambda.Term
if ($changeFunc -or $changeTerm)
{return $Index, $true, (New-LambdaApplication $func $term)}
return $Index, $false, $Lambda
}
if ($Index -ne 1)
{
$Index--
$Index, $changeFunc, $func = ConvertLambdaBeta $Index $Lambda.Function
$Index, $changeTerm, $term = ConvertLambdaBeta $Index $Lambda.Term
if ($changeFunc -or $changeTerm)
{return $Index, $true, (New-LambdaApplication $func $term)}
return $Index, $false, $Lambda
}
return -1, $true, (
Convert-LambdaSubstitution `
$Lambda.Function.Variable.Name `
$Lambda.Term `
$Lambda.Function.Term)
}
Lambda.Abstraction {
$Index, $change, $term = ConvertLambdaBeta $Index $Lambda.Term
if ($change)
{return $Index, $true, (New-LambdaAbstraction ($Lambda.Variable) $term)}
return $Index, $false, $Lambda
}
default {throw}
}
}
filter Convert-LambdaBetaNormalForm
{
Param
(
[Parameter(Mandatory=$true, ValueFromPipeline=$true)]
[PSTypeName("Lambda")] $Lambda,
[switch] $Step
)
$change = $true
$l = $Lambda
while ($change)
{
if ($Step) {$l}
$i, $change, $l = ConvertLambdaBeta 1 $l
}
if (-not $Step) {$l}
}
Set-Alias \ New-Lambda
Set-Alias \str Get-LambdaString
Set-Alias \var Get-LambdaVariable
Set-Alias \alpha Convert-LambdaAlpha
Set-Alias \sub Convert-LambdaSubstitution
Set-Alias \beta Convert-LambdaBeta
Set-Alias \bnf Convert-LambdaBetaNormalForm
Export-ModuleMember `
-Function @(
"*-Lambda*"
) `
-Alias @(
"\*"
)
$here = Split-Path -Parent $MyInvocation.MyCommand.Path
$sut = (Split-Path -Leaf $MyInvocation.MyCommand.Path) -replace '\.Tests\.', '.' -replace '\.ps1', '.psm1'
Import-Module "$here\$sut" -Force
Describe "Church Numerals" {
$cSucc = \ n f x . f (\ n f x)
$cPlus = \ m n . n $cSucc m
$cMult = \ m n f . m (\ n f)
$cExp = \ m n f x . (\ n m) f x
$cPred = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
$cMinus = \ m n . n $cPred m
$c0 = \ f x . x
$c1 = \ $cSucc $c0 |\bnf
$c2 = \ $cSucc $c1 |\bnf
$c3 = \ $cSucc $c2 |\bnf
It "Init" {$True | Should Be $True}
Context "Succ" {
It "0" {
$c0 |\bnf |\str | Should Be "\ f x . x"
}
It "1" {
$c1 |\bnf |\str | Should Be "\ f x . f x"
}
It "2" {
$c2 |\bnf |\str | Should Be "\ f x . f (\ f x)"
}
It "3" {
$c3 |\bnf |\str | Should Be "\ f x . f (\ f (\ f x))"
}
}
Context "Plus" {
It "0 + 0" {
\ $cPlus $c0 $c0 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "0 + 2" {
\ $cPlus $c0 $c2 |\bnf |\str | Should Be ($c2 |\bnf |\str)
}
It "3 + 0" {
\ $cPlus $c3 $c0 |\bnf |\str | Should Be ($c3 |\bnf |\str)
}
It "2 + 3" {
\ $cPlus $c2 $c3 |\bnf |\str | Should Be "\ f x . f (\ f (\ f (\ f (\ f x))))"
}
}
Context "Mult" {
It "0 * 0" {
\ $cMult $c0 $c0 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "0 * 2" {
\ $cMult $c0 $c2 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "3 * 0" {
\ $cMult $c3 $c0 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "1 * 1" {
\ $cMult $c1 $c1 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
It "1 * 2" {
\ $cMult $c1 $c2 |\bnf |\str | Should Be ($c2 |\bnf |\str)
}
It "3 * 1" {
\ $cMult $c3 $c1 |\bnf |\str | Should Be ($c3 |\bnf |\str)
}
It "2 * 3" {
\ $cMult $c2 $c3 |\bnf |\str |
Should Be "\ f x . f (\ f (\ f (\ f (\ f (\ f x)))))"
}
}
Context "exp" {
It "0 ^ 2" {
\ $cExp $c0 $c2 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "3 ^ 0" {
\ $cExp $c3 $c0 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
It "1 ^ 1" {
\ $cExp $c1 $c1 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
It "1 ^ 2" {
\ $cExp $c1 $c2 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
It "3 ^ 1" {
\ $cExp $c3 $c1 |\bnf |\str | Should Be ($c3 |\bnf |\str)
}
It "2 ^ 3" {
\ $cExp $c2 $c3 |\bnf |\str |
Should Be "\ f x . f (\ f (\ f (\ f (\ f (\ f (\ f (\ f x)))))))"
}
}
Context "Pred" {
It "Pred 0" {
\ $cPred $c0 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "Pred 1" {
\ $cPred $c1 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "Pred 2" {
\ $cPred $c2 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
It "Pred 3" {
\ $cPred $c3 |\bnf |\str | Should Be ($c2 |\bnf |\str)
}
}
Context "Minus" {
It "0 - 0" {
\ $cMinus $c0 $c0 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "0 - 2" {
\ $cMinus $c0 $c2 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "3 - 0" {
\ $cMinus $c3 $c0 |\bnf |\str | Should Be ($c3 |\bnf |\str)
}
It "2 - 3" {
\ $cMinus $c2 $c3 |\bnf |\str | Should Be ($c0 |\bnf |\str)
}
It "3 - 2" {
\ $cMinus $c3 $c2 |\bnf |\str | Should Be ($c1 |\bnf |\str)
}
}
}
Describe "Church Booleans" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cAnd = \ p q . p q p
$cOr = \ p q . p p q
$cNot = \ p a b . p b a
$cXor = \ a b . a (\ $cNot b) b
$cIf = \ p a b . p a b
It "Init" {$True | Should Be $True}
Context "If" {
It "True" {
\ $cIf $cTrue x y |\bnf |\str | Should Be "\ x"
}
It "False" {
\ $cIf $cFalse x y |\bnf |\str | Should Be "\ y"
}
}
Context "And" {
It "F And F" {\ $cAnd $cFalse $cFalse |\bnf |\str | Should Be ($cFalse | \str)}
It "F And T" {\ $cAnd $cFalse $cTrue |\bnf |\str | Should Be ($cFalse | \str)}
It "T And F" {\ $cAnd $cTrue $cFalse |\bnf |\str | Should Be ($cFalse | \str)}
It "T And T" {\ $cAnd $cTrue $cTrue |\bnf |\str | Should Be ($cTrue | \str)}
}
Context "Or" {
It "F Or F" {\ $cOr $cFalse $cFalse |\bnf |\str | Should Be ($cFalse | \str)}
It "F Or T" {\ $cOr $cFalse $cTrue |\bnf |\str | Should Be ($cTrue | \str)}
It "T Or F" {\ $cOr $cTrue $cFalse |\bnf |\str | Should Be ($cTrue | \str)}
It "T Or T" {\ $cOr $cTrue $cTrue |\bnf |\str | Should Be ($cTrue | \str)}
}
Context "Not" {
It "Not F" {\ $cNot $cFalse |\bnf |\str | Should Be ($cTrue | \str)}
It "Not T" {\ $cNot $cTrue |\bnf |\str | Should Be ($cFalse | \str)}
}
Context "Xor" {
It "F Xor F" {\ $cXor $cFalse $cFalse |\bnf |\str | Should Be ($cFalse | \str)}
It "F Xor T" {\ $cXor $cFalse $cTrue |\bnf |\str | Should Be ($cTrue | \str)}
It "T Xor F" {\ $cXor $cTrue $cFalse |\bnf |\str | Should Be ($cTrue | \str)}
It "T Xor T" {\ $cXor $cTrue $cTrue |\bnf |\str | Should Be ($cFalse | \str)}
}
}
Describe "Predicates" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cAnd = \ p q . p q p
$cSucc = \ n f x . f (\ n f x)
$cPred = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
$cMinus = \ m n . n $cPred m
$c0 = \ f x . x
$c1 = \ $cSucc $c0 |\bnf
$c2 = \ $cSucc $c1 |\bnf
$c3 = \ $cSucc $c2 |\bnf
$cIsZero = \ n . n (\ x . $cFalse) $cTrue
$cLEQ = \ m n . $cIsZero (\ $cMinus m n) |\bnf
$cEQ = \ m n . $cAnd (\ $cLEQ m n) (\ $cLEQ n m) |\bnf
It "Init" {$True | Should Be $True}
Context "is zero" {
It "0" {
\ $cIsZero $c0 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "1" {
\ $cIsZero $c1 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
It "2" {
\ $cIsZero $c2 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
}
Context "less-than-or-equal-to" {
It "0 leq 0" {
\ $cLEQ $c0 $c0 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "0 leq 1" {
\ $cLEQ $c0 $c1 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "1 leq 0" {
\ $cLEQ $c1 $c0 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
It "1 leq 1" {
\ $cLEQ $c1 $c1 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "2 leq 3" {
\ $cLEQ $c2 $c3 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "3 leq 2" {
\ $cLEQ $c3 $c2 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
}
Context "equals" {
It "0 eq 0" {
\ $cEQ $c0 $c0 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "0 eq 1" {
\ $cEQ $c0 $c1 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
It "1 eq 0" {
\ $cEQ $c1 $c0 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
It "1 eq 1" {
\ $cEQ $c1 $c1 |\bnf |\str | Should Be ($cTrue |\bnf |\str)
}
It "2 eq 3" {
\ $cEQ $c2 $c3 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
It "3 eq 2" {
\ $cEQ $c2 $c3 |\bnf |\str | Should Be ($cFalse |\bnf |\str)
}
}
}
Describe "Church pairs" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cPair = \ x y f . f x y
$cFirst = \ p . p $cTrue
$cSecond = \ p . p $cFalse
It "Init" {$True | Should Be $True}
It "First" {
\ $cFirst (\ $cPair p1 p2) |\bnf |\str | Should Be "\ p1"
}
It "Second" {
\ $cSecond (\ $cPair p1 p2) |\bnf |\str | Should Be "\ p2"
}
}
Describe "Two pairs as a list node" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cPair = \ x y f . f x y
$cFirst = \ p . p $cTrue
$cSecond = \ p . p $cFalse
$cNil = \ $cPair $cTrue $cTrue |\bnf
$cIsNil = $cFirst
$cCons = \ h t . $cPair $cFalse (\ $cPair h t) |\bnf
$cHead = \ z . $cFirst (\ $cSecond z) |\bnf
$cTail = \ z . $cSecond (\ $cSecond z) |\bnf
$e1N = \ $cCons e1 $cNil |\bnf
$e2e1N = \ $cCons e2 $e1N |\bnf
It "Init" {$True | Should Be $True}
Context "Is Nil" {
It "Nil" {
\ $cIsNil $cNil |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e1 nil" {
\ $cIsNil $e1N |\bnf |\str | Should Be ($cFalse | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cIsNil $e2e1N |\bnf |\str | Should Be ($cFalse | \str)
}
}
Context "Head" {
It "Cons e1 nil" {
\ $cHead $e1N |\bnf |\str | Should Be "\ e1"
}
It "Cons e2 (Cons e1 nil)" {
\ $cHead $e2e1N |\bnf |\str | Should Be "\ e2"
}
}
Context "Tail" {
It "Cons e1 nil" {
\ $cIsNil (\ $cTail $e1N) |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cTail $e2e1N |\bnf |\str | Should Be ($e1N | \str)
}
}
}
Describe "One pair as a list node" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cPair = \ x y f . f x y
$cFirst = \ p . p $cTrue
$cSecond = \ p . p $cFalse
$cCons = $cPair
$cHead = $cFirst
$cTail = $cSecond
$cNil = $cFalse
$cIsNil = \ l . l (\ h t d . $cFalse) $cTrue
$e1N = \ $cCons e1 $cNil |\bnf
$e2e1N = \ $cCons e2 $e1N |\bnf
It "Init" {$True | Should Be $True}
Context "Is Nil" {
It "Nil" {
\ $cIsNil $cNil |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e1 nil" {
\ $cIsNil $e1N |\bnf |\str | Should Be ($cFalse | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cIsNil $e2e1N |\bnf |\str | Should Be ($cFalse | \str)
}
}
Context "Head" {
It "Cons e1 nil" {
\ $cHead $e1N |\bnf |\str | Should Be "\ e1"
}
It "Cons e2 (Cons e1 nil)" {
\ $cHead $e2e1N |\bnf |\str | Should Be "\ e2"
}
}
Context "Tail" {
It "Cons e1 nil" {
\ $cIsNil (\ $cTail $e1N) |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cTail $e2e1N |\bnf |\str | Should Be ($e1N | \str)
}
}
}
Describe "Represent the list using right fold" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cPair = \ x y f . f x y
$cFirst = \ p . p $cTrue
$cSecond = \ p . p $cFalse
$cNil = $cFalse
$cIsNil = \ l . l (\ h t . $cFalse) $cTrue
$cCons = \ h t c n . c h (\ t c n)
$cHead = \ l . l (\ h t . h) $cFalse
$cTail = \ l c n . l (\ h t g . g h (\ t c)) (\ t . n) (\ h t . t)
$e1N = \ $cCons e1 $cNil |\bnf
$e2e1N = \ $cCons e2 $e1N |\bnf
It "Init" {$True | Should Be $True}
Context "Is Nil" {
It "Nil" {
\ $cIsNil $cNil |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e1 nil" {
\ $cIsNil $e1N |\bnf |\str | Should Be ($cFalse | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cIsNil $e2e1N |\bnf |\str | Should Be ($cFalse | \str)
}
}
Context "Head" {
It "Cons e1 nil" {
\ $cHead $e1N |\bnf |\str | Should Be "\ e1"
}
It "Cons e2 (Cons e1 nil)" {
\ $cHead $e2e1N |\bnf |\str | Should Be "\ e2"
}
}
Context "Tail" {
It "Cons e1 nil" {
\ $cIsNil (\ $cTail $e1N) |\bnf |\str | Should Be ($cTrue | \str)
}
It "Cons e2 (Cons e1 nil)" {
\ $cTail $e2e1N |\bnf |\str | Should Be ($e1N | \str)
}
}
}
Describe "Division" {
$cSucc = \ n f x . f (\ n f x)
$cPred = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
$cMinus = \ m n . n $cPred m
$cTrue = \ a b . a
$cFalse = \ a b . b
$cIsZero = \ n . n (\ x . $cFalse) $cTrue
$c0 = \ f x . x
$cY = \ f . (\ x . x x) (\ x . f (\ x x))
$cDiv = \ c n m f x . (\ d . $cIsZero d (\ $c0 f x) (\ f (\ c d m f x))) (\ $cMinus n m) |\bnf
$cDivide1 = \ $cY $cDiv
$cDivide = \ n . $cDivide1 (\ $cSucc n)
$c1 = \ $cSucc $c0 |\bnf
$c2 = \ $cSucc $c1 |\bnf
It "Init" {$True | Should Be $True}
It "2 / 2" {
\ $cDivide $c2 $c2 |\bnf |\str | Should Be ($c1 |\str)
}
}
Describe "Signed numbers" {
$cTrue = \ a b . a
$cFalse = \ a b . b
$cPair = \ x y f . f x y
$cFirst = \ p . p $cTrue
$cSecond = \ p . p $cFalse
$cSucc = \ n f x . f (\ n f x)
$cPlus = \ m n . n $cSucc m
$cMult = \ m n f . m (\ n f)
$cPred = \ n f x . n (\ g h . h (\ g f)) (\ u . x) (\ u . u)
$cMinus = \ m n . n $cPred m
$cIsZero = \ n . n (\ x . $cFalse) $cTrue
$c0 = \ f x . x
$c1 = \ $cSucc $c0 |\bnf
$c2 = \ $cSucc $c1 |\bnf
$c3 = \ $cSucc $c2 |\bnf
$c4 = \ $cSucc $c3 |\bnf
$cY = \ f . (\ x . x x) (\ x . f (\ x x))
$cConvert_s = \ x . $cPair x $c0
$cNeg_s = \ x . $cPair (\ $cSecond x) (\ $cFirst x)
$c_0_0 = \ $cConvert_s $c0 |\bnf
$c_1_0 = \ $cConvert_s $c1 |\bnf
$c_0_1 = \ $cNeg_s $c_1_0 |\bnf
$c_1_1 = \ $cPair $c1 $c1 |\bnf
$c_2_0 = \ $cConvert_s $c2 |\bnf
$c_0_2 = \ $cNeg_s $c_2_0 |\bnf
$c_0_4 = \ $cNeg_s (\ $cConvert_s $c4) |\bnf
$cOneZ = \ c xx . $cIsZero (\ $cFirst xx) xx (\ $cIsZero (\ $cSecond xx) xx (\ c $cPair (\ $cPred (\ $cFirst xx)) (\ $cPred (\ $cSecond xx))))
$cOneZero = \ $cY $cOneZ |\bnf
$cPlus_s = \ xx yy . $cOneZero (\ $cPair (\ $cPlus (\ $cFirst xx) (\ $cFirst yy)) (\ $cPlus (\ $cSecond xx) (\ $cSecond yy))) |\bnf
$cMinus_s = \ xx yy . $cOneZero (\ $cPair (\ $cPlus (\ $cFirst xx) (\ $cSecond yy)) (\ $cPlus (\ $cSecond xx) (\ $cFirst yy))) |\bnf
$cMult_s = \ xx yy . $cPair (\ $cPlus (\ $cMult (\ $cFirst xx) (\ $cFirst yy)) (\ $cMult (\ $cSecond xx) (\ $cSecond yy))) (\ $cPlus (\ $cMult (\ $cFirst xx) (\ $cSecond yy)) (\ $cMult (\ $cSecond xx) (\ $cFirst yy))) |\bnf
$cDiv = \ c n m f x . (\ d . $cIsZero d (\ $c0 f x) (\ f (\ c d m f x))) (\ $cMinus n m) |\bnf
$cDivide1 = \ $cY $cDiv
$cDivide = \ n . $cDivide1 (\ $cSucc n)
$cDivZ = \ x y . $cIsZero y $c0 (\ $cDivide x y)
$cDivide_s = \ xx yy . $cPair (\ $cPlus (\ $cDivZ (\ $cFirst xx) (\ $cFirst yy)) (\ $cDivZ (\ $cSecond xx) (\ $cSecond yy))) (\ $cPlus (\ $cDivZ (\ $cFirst xx) (\ $cSecond yy)) (\ $cDivZ (\ $cSecond xx) (\ $cFirst yy)))
It "Init" {$True | Should Be $True}
Context "OneZero" {
It "(0, 0)" {
\ $cOneZero $c_0_0 |\bnf |\str | Should Be ($c_0_0 |\str)
}
It "(0, 1)" {
\ $cOneZero $c_0_1 |\bnf |\str | Should Be ($c_0_1 |\str)
}
It "(1, 0)" {
\ $cOneZero $c_1_0 |\bnf |\str | Should Be ($c_1_0 |\str)
}
It "(1, 1)" {
\ $cOneZero $c_1_1 |\bnf |\str | Should Be ($c_0_0 |\str)
}
}
Context "Plus" {
It "(+ 1) + (+ 1)" {
\ $cPlus_s $c_1_0 $c_1_0 |\bnf |\str | Should Be ($c_2_0 |\str)
}
It "(+ 1) + (- 1)" {
\ $cPlus_s $c_1_0 $c_0_1 |\bnf |\str | Should Be ($c_0_0 |\str)
}
It "(- 1) + (+ 1)" {
\ $cPlus_s $c_0_1 $c_1_0 |\bnf |\str | Should Be ($c_0_0 |\str)
}
It "(- 1) + (- 1)" {
\ $cPlus_s $c_0_1 $c_0_1 |\bnf |\str | Should Be ($c_0_2 |\str)
}
}
Context "Minus" {
It "(+ 1) - (+ 1)" {
\ $cMinus_s $c_1_0 $c_1_0 |\bnf |\str | Should Be ($c_0_0 |\str)
}
It "(+ 1) - (- 1)" {
\ $cMinus_s $c_1_0 $c_0_1 |\bnf |\str | Should Be ($c_2_0 |\str)
}
It "(- 1) - (+ 1)" {
\ $cMinus_s $c_0_1 $c_1_0 |\bnf |\str | Should Be ($c_0_2 |\str)
}
It "(- 1) - (- 1)" {
\ $cMinus_s $c_0_1 $c_0_1 |\bnf |\str | Should Be ($c_0_0 |\str)
}
}
Context "Multiply" {
It "(- 2) * (+ 2)" {
\ $cMult_s $c_0_2 $c_2_0 |\bnf |\str | Should Be ($c_0_4 |\str)
}
}
Context "Division" {
It "(- 2) / (+ 2)" {
\ $cDivide_s $c_0_2 $c_2_0 |\bnf |\str | Should Be ($c_0_1 |\str)
}
}
}
@SoptikHa2
Copy link

Wow. Is there context to this gist?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment