Last active
May 11, 2020 15:33
-
-
Save yumura/d22146f63fea915391e090205810ccdf to your computer and use it in GitHub Desktop.
Lambda calculus :: PowerShell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 @( | |
| "\*" | |
| ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $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) | |
| } | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Wow. Is there context to this gist?