Last active
September 5, 2023 01:44
SATySFiでアッカーマン関数
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
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
@require: stdja | |
@require: list | |
@require: math | |
let-rec ack | |
| 0 n = n + 1 | |
| m 0 = ack (m - 1) 1 | |
| m n = ack (m - 1) (ack m (n - 1)) | |
type aexpr = | |
| Num of int | |
| Fun of aexpr * aexpr | |
let-rec calc1 | |
| (Num(n)) = Num(n) | |
| (Fun(Num(0), Num(n))) = Num(n + 1) | |
| (Fun(Num(m), Num(0))) = Fun(Num(m - 1), Num(1)) | |
| (Fun(Num(m), Num(n))) = Fun(Num(m - 1), Fun(Num(m), Num(n - 1))) | |
| (Fun(x, y)) = Fun(x, calc1(y)) | |
let calc-all e0 = | |
let-rec repeat e a = | |
match e with | |
| Num(_) -> List.reverse (e :: a) | |
| _ -> repeat (calc1 e) (e :: a) | |
in | |
repeat e0 [] | |
let-rec aexpr2str | |
| (Num(n)) = (arabic n) | |
| (Fun(x, y)) = `A(` ^ (aexpr2str x) ^ `,` ^ (aexpr2str y) ^ `)` | |
let-rec expr2math | |
| (Num(n)) = math-char MathOrd (arabic n) | |
| (Fun(x, y)) = | |
let x = expr2math x in | |
let y = expr2math y in | |
${A\( #x, #y \)} | |
let-block ctx +eqns mlst = | |
let em = embed-math ctx in | |
let print ib = line-break true true ctx (ib ++ inline-fil) in | |
match mlst with | |
| [] -> block-nil | |
| f::[] -> print (em f) | |
| f::(s::r) -> | |
let margin = match space-between-maths ctx f ${=} with | |
| None -> inline-nil | |
| Some(ibsp) -> ibsp | |
in | |
let indent = inline-skip (get-natural-width (em f)) ++ margin in | |
let p m = print (indent ++ (em ${= #m})) in | |
List.map p r | |
|> List.fold-left (+++) (print (em ${#f = #s})) | |
let-block ctx +Ack m n = | |
let ms = Fun(Num(m), Num(n)) | |
|> calc-all | |
|> List.map expr2math | |
in | |
read-block ctx '<+eqns(ms);> | |
let-block ctx +ctx conf bt = | |
let c = List.fold-left (fun c f -> f c) ctx conf in | |
read-block c bt | |
in | |
document (| | |
title = {Ackermann function}; | |
author = {youz}; | |
show-title = false; | |
show-toc = false; | |
|) '< | |
+ctx[ | |
set-paragraph-margin 8pt 8pt | |
] < | |
+Ack(3)(1); | |
> | |
> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment